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

✍️source

#agent #compiler #diagram #formal #llvm #makefile #news #optimization #rust #sec
- Lightweight Diagramming for Lightweight Formal Methods
- #perf
    - Why doesn’t Rust care more about compiler performance?
    - One Law to Rule All Code Optimizations
    - Simulating Time With Square-Root Space
    - Is Rust faster than C?
    - Revisiting Knuth’s “Premature Optimization” Paper
- #os
    - Asterinas: A Linux ABI-compatible, Rust-based framekernel OS #rust
        - framekernel: the performance of a monolithic kernel and the security of a microkernel
        - OSTD, an OS framework, so that a Hello World kernel in 100 lines of safe Rust
        - TCB (Trusted Computing Base) is the minimal unsafe code required to build a kernel in safe Rust
            - ~15K LOC, 14- rich OS features
        - aims to verify unsafe code with Verus
        - uses model checking with Converos to uncover hard-to-find concurrency bugs
        - see also Asterinas: a new Linux-compatible kernel project
    - Blog series on creating an OS in Rust (on HN) #rust
    - Starina - A modern general-purpose microkernel OS
        - from Building Linux kernel on macOS natively (on HN)
            - Clang Built Linux effort helped to build Linux kernel with clang + LLVM instead of GCC + GNU
            - it seems to work and is simple enough, I should try it sometimes
    - Munal OS: A graphical experimental OS with WASM sandboxing
        - written in Rust
        - embeds wasmi
        - no virtual address space as userspace is inside WASM sandbox
        - only VirtIO so it runs only in an VM
        - has links to OS dev resources
    - Talos: a container optimized Linux distro, which is declarative, immutable, secure
        - minimal: consists of only a handful of binaries and shared libraries: just enough to run containerd and a small set of system services
            - written in Go
        - no SSH and console access, fully controlled by API via gRPC
        - Which Kubernetes is the Smallest? Examining Talos Linux, K3s, K0s, and More
            - Talos has the minimal footprint
    - The high-level OS challenge
    - A DOS-like hobby OS written in Rust and x86 assembly
        - RoureXOS rewritten in Rust
    - Tilck: A Tiny Linux-Compatible Kernel (on HN)
- Makefile.md - Possibly Use(ful|less) Polyglot Synthesis of Makefile and Markdown
- comments on Qwen3 embedding models
- #prolog
    - from Readings shared June 9, 2025
    - Teaching and learning mathematics with Prolog
    - Exploring Topological Spaces with Prolog: A Practical Approach Using “Mathematics with Prolog”