[codebje]

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.

[4ad]

Dafny is great, and has some advantages compared to its competitors, but unequivocally calling it "the best" is quite bullish. For example, languages using dependent types (F*, ATS, Coq/Adga/Lean) are more expressive. And there are very mature systems using HOL.

Truth is that everything involves a tradeoff, and some systems are better than others at different things. Dafny explores a particular design space. Hoare-style invariants are easier to use than dependent types (as long as your SMT solver is happy, anyway) but F* also has that, except that in F* you can also use dependent types when automatic refinement proofs become inadequate. And F* and ATS can target low-level, more so than Dafny.

Probably I would not use ATS for anything, but between F* and Dafny, there isn't such a clear cut (I'd most likely use F*).

And if I don't need (relatively) low-level, I wouldn't use either.

[codebje]

Ah, my apologies, I wasn't particularly clear. The "best" I am referring to is only code generation into popularly used languages.

I'm currently using Lean myself, but Agda's probably going to win out longer term for me simply because it compiles to GHC Haskell.

[Xmd5a]

Can't I just work on a subset of the language? I don't care if the linked list implementation I use isn't verified. I want to verify my own code, not because it will run on mars, but as an alternative to writing tests. Is this possible?

[Jtsummers]

Yes. See SPARK for an example of this. It is a subset of Ada plus the SPARK portions to convey details and proofs. You can use it per file, not just on an entire program, which lets you prove properties of critical parts and leave the rest to conventional testing approaches.

[4ad]

Unless you use a language designed for formal verification (Lean/Idris/Agda/F*/ATS/etc), no, it is not possible.

You can get pretty far in Haskell (with various extensions) and Scala. But for Go/TypeScript/etc, forget about it.