Do I want to learn Dafny?

Brian Hicks, July 28, 2023

So I recently learned about Dafny. From my notes on it, I summarized it as:

a verified programming language. That is, you can write a program with preconditions, postconditions, proofs, etc and then export that code to C#, Java, JavaScript, and Go (with more languages coming.)

I'm curious about this! Getting better tools for writing reliable software feels intrinsically good to me. After all, even if I'm not working on the space shuttle or medical equipment where bugs are life-threatening, they can still be costly and annoying.

That said, I also know that correctness is not the only goal in software engineering. For example: right now, I'm working on software for work that we hope will be useful to expand into a new market segment (from high schools to upper elementary schools.) At the moment, it's less important that the software I'm writing be correct, and more important that it just exist. We can work out the bugs after we figure out what's most valuable to classroom teachers!

But what if it was faster to write correct software? That sure would open up some things for me to explore!

So, maybe it's worth looking into Dafny? I see there are some books that have to do with proving theorems generally which may be useful learning… I remember when I've tried other systems like this (notably Coq but also Idris to a lesser extent) I've really been fumbling around in the dark trying to get programs proved. I wonder if having more foundational knowledge would help?

Anyway, I think I'll give it a go, at least for a bit!