I agree, using tools more in line with your language is better but I believe the knowledge from learning Dafny ought to transfer well to other systems. And Dafny seems better as a pedagogical system than what I've seen and used for other languages.

I'm exploring it now as a way to ease colleagues into SPARK. A lot of the material appears to transfer over and the book Program Proofs seems better to me than what I found for SPARK. I probably wouldn't have colleagues work through the book themselves so much as run a series of tutorials. We've done this often in the past when trying to bring everyone up to speed on some new skillset or tooling, if someone already knows it (or has the initiative to learn ahead of time) then they run tutorial sessions every week or so for the team.

https://github.com/verus-lang/verus is similar tool for Rust (developed by previous heavy users of Dafny).

The languages people already use are inconsistent (in a logic theory sense) and lack formal semantics. Efforts to try and prove anything useful about programs written in those languages don't get far, because the first fact requires you to restrict everything to a subset of the languages, and sometimes that restricts you to an unworkable subset, and the latter fact is a massive hill to climb at whose peak is a note saying, "we have changed the implementation, this hill is no longer relevant."

The only* practical way to approach this is exactly Dafny: start with a (probably) consistent core language with well understood semantics, build on a surface language with syntax features that make it more pleasant to use, proving that the surface language has a translation to the core language that means semantics are clear, and then generate the desired final language after verification has succeeded.

Dafny's about the best of the bunch for this too, for the set of target languages it supports.

(It's fine and normal for pragmatic languages to be inconsistent: all that means here is you can prove false is true, which means you can prove anything and everything trivially, but it also means you can tell the damn compiler to accept your code you're sure is right even though the compiler tells you it isn't. It looks like type casts, "unsafe", and the like.)

* one could alternatively put time and effort into making consistent and semantically clear languages compile efficiently, such that they're worth using directly.

The only tool I see to ever take off in languages that people already use is design by contract, and is has been a hard ride even making that available in some.

Let alone something more complex in formal verification.

I am not a Dafny expert but from what I have gathered it uses a deductive procedure underneath, so it's rather geared towards sequential code. To analyse concurrent code, one needs to essentially build a sequential program that _also models the scheduler_ (see e.g., [1]).

This procedure is unsurprisingly called sequentialization and (somewhat less unsurprisingly) is also a pretty good approach when applied to other techniques, such as bounded model checking [2].

[1] https://leino.science/papers/krml260.pdf

[2] https://research.cs.wisc.edu/wpis/papers/cav08.pdf

Comparison with TLA+ doesn't make any sense as TLA+ implements a very different sort of logic, but the property that it is a real programming language is shared by virtually everything in this space.

Lean/Adga are real programming languages, while Coq (Rocq), F*, ATS, Isabelle/HOL all extract to various other programming languages.

Frankly, it's TLA+ that is the odd one here.

the problem I had with Dafny was the automated prover abruptly driving off a complexity cliff. the strategy is to build "tactic" functions that don't run at runtime but discharge a proof obligation at compile time.

I'd be ecstatic if LLMs could write those tactic functions. Unfortunately, they're not great at the reasoning and preciseness required (plus their training data isn't exactly overflowing with Dafny proofs.)