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…

Commenting on Bubbles has been removed. Why? If you want to talk about this post, write to the author, use the comments on their blog if it has them, or reply with a "RE:" post on your own blog. Suggestions? feedback@bubbles.town