IO for Software Design

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 poking around a bit I decided to give Dafny a try, only to find that its standard library has gaps too. Depending on whether or not I’m able to find work, I might try to recruit some undergrads to fill those in. What follows is a spec for what I would need them to build in order to be able to replicate the examples in the existing books. In brief: Dafny’s standard library provides only whole-file I/O…