The problem with Dafny and other SMT solvers is that when they work, they're brilliant, but when they don't, they're infuriating.
Sometimes your code and theorems are formed in a way which Dafny is very good at reasoning about (e.g. standard induction). Then it's nice to just write code and have everything verify.
Other times your assertions are non-trivial to the verifier, even if they look obvious, and you must write lemmas and assertions to get them to be proven. And the problem with SMT solvers is that it can be hard to figure out which lemmas and assertions you need to add. It's frustrating to see some assertion Dafny can't prove, which to you seems almost self-evident, and it can be hard to see what is missing.
Languages like Coq, Lean, and Isabelle/HOL are better in that you prove things manually (unless you abuse `auto` and tactics for non-trivial proofs, then you still run into the above). Because when you're writing a manual proof, you know exactly what you have and what you need to prove and why the two aren't yet the same. It can still be frustrating but less so, because in Coq you usually have a better idea what key details are unproven, whereas in Dafny you just get "this (entire statement) can't be proved". You could also say that Coq goes "above and beyond" even though you must write the proofs manually, because you can statically check arbitrary properties and write "safe" code which upholds extremely complex invariants using dependent types.
But ultimately, any formal verification language becomes extremely verbose and challenging to write once the properties you are trying to statically prove become mildly complicated. Which is why most code doesn't go "above and beyond" even though formal methods have been around for decades. It's an unfortunate reality in the field: you can spend decades writing a formally-verified version of a medium-sized program, or could spend weeks writing the program itself and then writing solid tests (see: CompCert, sel4). But I still think we're making progress: case in point Rust (and other new languages with ownership semantics), and companies actually using formal methods to verify the small but critical parts of your code.
> The problem with Dafny and other SMT solvers is that when they work, they're brilliant, but when they don't, they're infuriating
Yeah, look I'm not going to disagree with that. I have had plenty of frustrating times figuring out why something won't verify with Dafny. But, the more you do it, the easier it gets. And, we should work on the assumption that these tools will get better.
> Languages like Coq, Lean, and Isabelle/HOL are better in that you prove things manually (unless you abuse `auto` and tactics for non-trivial proofs, then you still run into the above).
So, it is nice that you always feel like you can make progress with these tools. But, at the same time, that progress can be awfully slow and painstaking. I think the sweet spot lies in using automation as much as possible, but with the fall back option of proving things manually. Dafny to some extent lets you do this, as you can always fall back on manual induction using a lemma.
Sometimes your code and theorems are formed in a way which Dafny is very good at reasoning about (e.g. standard induction). Then it's nice to just write code and have everything verify.
Other times your assertions are non-trivial to the verifier, even if they look obvious, and you must write lemmas and assertions to get them to be proven. And the problem with SMT solvers is that it can be hard to figure out which lemmas and assertions you need to add. It's frustrating to see some assertion Dafny can't prove, which to you seems almost self-evident, and it can be hard to see what is missing.
Languages like Coq, Lean, and Isabelle/HOL are better in that you prove things manually (unless you abuse `auto` and tactics for non-trivial proofs, then you still run into the above). Because when you're writing a manual proof, you know exactly what you have and what you need to prove and why the two aren't yet the same. It can still be frustrating but less so, because in Coq you usually have a better idea what key details are unproven, whereas in Dafny you just get "this (entire statement) can't be proved". You could also say that Coq goes "above and beyond" even though you must write the proofs manually, because you can statically check arbitrary properties and write "safe" code which upholds extremely complex invariants using dependent types.
But ultimately, any formal verification language becomes extremely verbose and challenging to write once the properties you are trying to statically prove become mildly complicated. Which is why most code doesn't go "above and beyond" even though formal methods have been around for decades. It's an unfortunate reality in the field: you can spend decades writing a formally-verified version of a medium-sized program, or could spend weeks writing the program itself and then writing solid tests (see: CompCert, sel4). But I still think we're making progress: case in point Rust (and other new languages with ownership semantics), and companies actually using formal methods to verify the small but critical parts of your code.