Last winter I wrote a discrete event simulation framework in Python to keep myself busy, have something to put on my CV, experiment with LLM-assisted coding, and learn how async and await actually work. Over the summer, for similar reasons, I played around a bit with Lean and Gleam, thinking that I might translate the Software Design by Example books from JavaScript and Python into one or the other. Lean defeated me, and I quickly grew frustrated with the gaps in Gleam’s standard library, but my noodling around left me wanting to learn more about formal verification of programs. After...