My guy happened to come with a bow tie

Oh man and I totally forgot all the super cool work on OCaml’s new modal type system!

And finally, this was the first year I really started using Lean in anger. Lot’s of great work on making a proof assistant nice and ergonomic. It’s a really wonderful language to work in!

Cool and wacky work from Neil Walkinshaw on trying to get a formal solution to the “stopping problem” in random testing. arxiv.org/pdf/2405.17019. This formulation has a bunch of limitations/assumptions, but I really enjoy the framing and line of thought.

Google’s work on automating the creation of fuzz harnesses seems promising for lowering the barrier to robust software: security.googleblog.com/2023/08/ai-p...