December 2021 readings

I am starting an experiment: just document interesting things I read as a list from time to time. It’s already the twelvth, vacations are coming up, and I already did a lot of reading I haven’t documented, so I expect this month’s list to be pretty short.

Graphics

• A blog post, Physarum, by Sage Jenson — slime mold population generation, pretty cool looking.
• Re-read learn wgpu. Good tutorial!

Databases & Distributed Systems

• Don’t Get Stuck in the “Con” Game, by Pat Helland. Deconstruction of the notion of consistency and eventual consistency. Proposes more well defined notion to know what we talk about when we talk about consistency. A potentially useful toolbox for reasoning and exposition.

Formal Methods

• Rust verification tools (2021), by Alastair Reid. Alastair Reid’s updated list of automated verification tools for Rust. I’ve been interested for a long time, so not many projects were new, but I learned about shuttle, the Oxide paper, hacspec, SeaHorn and rust-horn from this. The companion blog post has interesting sections on the respective weaknesses of abstract interpretation, bounded model checkers, dynamic symbolic execution and instrumented interpreters like miri.

Math

• How real are real numbers? by Gregory Chaitin (2004). A very approachable, condensed, well exposed high level view of some problematic features of the real numbers, in particular from an intuitionistic perspective (Borel’s). First from a principle perspective, then linked to a formal perspective with the later emergence of computer science. Good read.

General blog posts / opinions

• Query-based compilers. The author draws connections between query-based compilers (examples: rust-analyzer, typescript) and the Build-systems à la carte paper. My personal impression is that there’s an analogy here with nix as well.