Dafny: Verification-Aware Programming Language

I quite like Dafny, despite my first run up with it (verification aspect) being frustrating. The language is well designed for this. Also, it looks like it is a great candidate as a code generation target for LLMs because you can generate the proof of correctness and run a feedback loop with Dafny's checker.

Try writing a^b in integers and proving its correctness. The simple version works (based on a x a^(b-1)). But if you write an "optimised one" using (with handwaved details) (a^(b/2))^2 .... pulled some serious hair trying to prove this function works.

This formal verification course I took by Manos Kapritsos and Jon Howell is taught in Dafny and assumes no former experience with the subject. Most of the exercises are to some degree “self-grading” as proof success means you have a correct solution, provided your spec is correct. I highly recommend.

https://glados-michigan.github.io/verification-class/fall202...

I got a bit into SPARK (a subset Ada of that has formal verification) with AoC, and while it can be tricky, SPARK is quite flexible in how much you prove. Dafny sounds interesting, but I can't find a comparison between the two. There's obviously a difference in memory management, but the rest looks quite similar at first sight, and their niche is quite similar. Does anyone know of a (deeper) comparison between both languages?

This might be a stupid question, but why a separate programming language rather than aiming to verify/synthesize invariants in languages people use?

This looks pretty neat, but the mapping to other languages looks rather awkward for string types (for example).

Fine for teaching, but it doesn't seem to be a suitable tool to generate idiomatic library code?

Looks interesting. I saw some C# files, from which it seems it is implemented in C#. Is there going to be an implementation in Dafny?

Reminds me of Eiffel, in a good way. Looks awesome. Is there anything close to this in Scala by chance?