NOTE: This site has just upgraded to Forester 5.x and is still having some style and functionality issues, we will fix them ASAP.

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

#cg #compiler #diagram #formal #game #optimization #os #proof #render #rust
- wrote Trying Zig's self-hosted x86 backend on Apple Silicon (on reddit)
- #lean
    - Premise Selection for a Lean Hammer
        - the paper behind LeanHammer
    - Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean
    - Trinity: an autoformalization system for verified superintelligence
    - Mathesis: Towards Formal Theorem Proving from Natural Languages
    - watched Mr. Mario Carneiro | Lean Meta-theory: The Proofs behind the Proofs
- Rewriting SymCrypt in Rust to modernize Microsoft’s cryptographic library
    - used Aeneas, a Verification Framework for Rust that supports F*, Coq, HOL4 and Lean
        - the team also built
            - Charon to extract information from rustc internals for semantic analysis thus verification
            - Eurydice, a Rust-to-C compiler to provide a backwards-compatibility story as the verification ecosystem gradually transitions to Rust
    - used Revizor - a fuzzer to search for microarchitectural leaks in CPUs
        - analyze binary code for specific compilers and platforms
        - find side channel vulnerabilities caused by timing leaks or speculative execution
        - which aren't visible in the source code
        - for today’s CPUs, every new optimization may open a new side channel, which renders constant-time programming insufficient
- found Lightweight Diagramming for Lightweight Formal Methods
    - formal methods help users define, explore, verify, and diagnose specifications for complex systems incrementally
    - Forge: A Tool and Language for Teaching Formal Methods
        - similar to Alloy 6
        - uses Sterling visualizer
    - Cope and Drag (CnD)
        - embedded in an open-source visualizer for Forge
        - focuses on encoding the spatial intuitions implicit in communicating the model
            - constraining spatial layout (such as positioning child nodes below their parents in a binary tree)
            - grouping elements (like clustering related components in a software architecture)
            - directing drawing style (for instance, coloring nodes in a red-black tree based on their color)
- #debugger
    - strace tips for better debugging
    - Demystifying Debuggers (a series)
    - Linus on Why Debuggers Are Actually Bad For Developers
    - found Building a Debugger: Write a Native x64 Debugger From Scratch
- #raku
    - Raku's "core"
    - Raku's FAQ
    - RakuAST: a foundation for Raku macros
    - Raku in y minutes
- Readings shared June 10, 2025
- realized that Pocoo is behind Sphinx, Jinja, Pygments etc.
- found Verse Language, a new scripting language for Fortnite by Epic