Learning diary › Year 2025 › June, 2025 › 2025-06-13 [2025-06-13]

✍️source

#benchmark #formal #lean #news #os #rss #rust #tui #z3 #zig
- Solving LinkedIn Queens with SMT
    - in Z3 SMT solver instead of CVC5 SMT solver as in Using SAT to Get the World Record on LinkedIn's Queens
    -  SAT solvers are "criminally underused by the industry" (from Modern SAT solvers: fast, neat and underused)
    - SMT solvers are "higher-level" than SAT, capable of handling more data types than just boolean variables
    - It's a lot easier to solve the problem at the SMT level than at the SAT level
    - people prefer SMT to SAT
    - Glucose, an SAT solver is really fast
    - The Hat, the Spectre and SAT Solvers (2024) (on HN) (on lobste.rs)
- jemalloc Postmortem
    - they "reached a sad end for jemalloc in the hands of Facebook/Meta even though most of the people involved were acting in good faith"
    - "the root of the problem is lack of awareness about external uses and needs"
        - even "unaware of its replacement until after the fact"
    - "internally siloed open source projects cannot thrive"
    - should evaluate alternatives
        - TCMalloc by Google (with Bazel painpoint)
        - mimalloc
            - adopted by CPython 3.12: "it is fast, thread-safe, and NUMA-aware"
        - StarMalloc: verified memory allocator
        - phkmalloc
- looking for best way to read Hacker News comments
    - most TUI are not working well for reading comments, see `just prep-hkt`
    - found Vue HN that supports dark theme, and groups comments, it works pretty well with Doubao auto-translation
    - found Hacker News RSS and chose the front page feed, and I have already subscribed to the best comments feed
- Could an LLM create a full Domain-Specific Language?
    - rather complete methodology for creating a DSL
    - code: jcabot/funding-dsl
- The last six months in LLMs, illustrated by pelicans on bicycles
    - an interesting benchmark for LLMs
- #ai-safety #env
    - AI Boom Drives 150% Surge in Indirect Emissions at Major Tech Firms, UN Warns
        - numbers for the environmental impact of LLMs
        - related
            - AI threatens to raid the water reserves of Europe's driest regions
    - Environmental Impacts of Artificial Intelligence
    - Mistral reports on the environmental impact of LLMs (on HN)
        - Simon Willison | Our contribution to a global environmental standard for AI
    - Problems the AI industry is not addressing adequately
    - Generative AI’s crippling and widespread failure to induce robust models of the world
- Type-based vs Value-based Reflection
    - value-based (C++26)
        - "while we have new syntax for getting into (`^^e`) and out of (`[: e :]`) the value domain, once you’re in the value domain — it’s nice to just stay there"
        - "C++26 reflection does bring with it new syntax and a bunch of new semantics. But the benefit is that a lot of metaprogramming starts to look more like regular programming. There is a lot less syntax in the implementation side of things. "
    - type-based (Reflection TS published in March, 2020)
    - wondering the Zig equivalent
    - Discover C++26’s compile-time reflection
    - C++26 Reflections adventures and compile-time UML
- Reflections on Sudoku, Or the Impossibility of Systematizing Thought
    - limitation of TDD
        - tests don't fix the underlying issue of "knowing what to do"
    - alternative approach by Peter Norvig
        - analyzing the high-level problem and then breaking down the data structures and outlining the solution in the course of ~20 lines of code
- found A Lightweight Merge Queue using GitHub Actions
- Rumour: Google intends to discontinue the Android Open Source Project
- A tale of two spacetimes
- In case of emergency, break glass
- skimmed Patterns for Modeling Overlapping Variant Data in Rust
- What I talk about when I talk about IRs