> 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.
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.