Dafny: Verification-Aware Programming Language

Am working on rewriting an imperative programming course to use Dafny to present verified algorithms and data structures.

Not a stupid question at all. There are two reasons verification tends to happen in these specialized languages: the languages we usually use are often not expressive enough to write things like specifications, and a bit too expressive in the sense of letting people write program logic that is insanely difficult to verify (think untyped pointers into a dynamically allocated heap for example). So these verification related languages often are more expressive on the spec side and more restrictive in terms of what kind of code you can write.

> … verify/synthesize invariants in languages people use?

Good question. This is the holy grail. This is what everyone in PL research would love. This is where we want to get to.

Turns out a language as “simple” as C has sufficiently complicated semantics as to limit rigorous analysis to the basics. One example is loop analysis: it’s very useful to know that a loop will terminate eventually; if a loop is modifying some state and—worse—if the iteration variable gets modified—kiss your analysis goodbye because mechanically synthesizing strong pre- and post-conditions becomes insurmountable. It’s not an engineering challenge. It’s a math/pure CS theory challenge.

Most existing mainstream languages aren’t expressive enough to encode these invariants. For languages outside of the mainstream, Lean 4 is a language supporting verification, and it’s also a full programming language, so you can write your proofs/theorems in the same language that you program in.

Dafny has been around for a while and people do in fact use it. People also apply contract languages to C and all matter of other things, so really question boils down to "Why arent you doing what I expect of you?"

The semantics of Dafny is carefully designed to make verification efficient.

Dafny can compile to and interface with a few languages, including C#.

It could be done, but what would be the virtue of it? Most programming languages are not self-hoisted for a reason.

Dafny is quite different from Scala in that it is a formal language that can be compiled to a number of different targets such as Go or Python or C#. This allows an algorithm to be formally verified while still producing executable code.

You could add Scala as a compilation target or you could just use the Java output and call formally verified Java functions from Scala. Even if you do get an implementation that produces Scala, don't expect the full power of idiomatic Scala to be available in the code you formally verify. To verify code, you have to write the code in Dafny with associated assertions to be proven. Since there are multiple compilation targets multiple formal constraints on what can usefully be verified, the data types available will not match the data types that you would use natively from Scala.

It's similar in spirit, but in Dafny one can express much more complicated and complex invariants which get checked at build time -- compared to eiffel where pre/post conditions are checked at runtime (in dev builds mostly).