Verified cryptography for Firefox 57 (opens in new tab)

F* is somewhat well known in circles of information security, but it's not widely used in general. It's frequently used for formal verification of cryptographic protocols. If you look at the papers on the website you'll see a variety of applications for provable security in crypto.

I wouldn't call it a general purpose language (in the sense that you can productively use it for just about anything), but to be fair I've only read papers about/using the language; I've not used it personally. It's a great leap forward for provable security in general, though.

F* is a great project and under very active development. Basically at every POPL you find papers with genuine improvements and simplifications to the core of F*. I don't know of any other language that's improving this rapidly.

> Here Mozilla is trying to verify it’s crypto.

If you look at the paper describing this work <https://arxiv.org/abs/1703.00053>, you'll see that this is an academic effort and 7 of 12 authors are actually at Microsoft Research. But kudos to Mozilla for bringing all this advanced stuff to their products.

> At minimum, we’ll need to see more user-friendly variants of TLA+ and other techniques for average developers to be able to use.

TLA+ is quite user-friendly, certainly more than most other formal methods. It takes about two weeks to become fully productive, without any guidance other than the freely available tutorials. It's easier to learn than most programming languages.

> Probably it should be taught in normal CS education.

I agree.

While this is a fun aphorism, it's getting less and less applicable these days since many proof systems (and programming languages that double as such) allow for code extraction to e.g. ML or C code. Naturally, the usual caveats apply: You'll want proof that the code extractor is correct. (But then, you'd want proof that the proof system itself is correct, regardless.)

Nevertheless, the aphorism is part of the reason that I'm (also) sceptical of using proof systems that don't allow for code extraction. Assuming you're actually trying to prove things about programs and just just proving things for e.g. math.

> a few thousands lines of code when I looked at it a while back.

That's not true anymore. Have a look at CompCert, CakeML or CertiKOS, for example. Verification still takes a big effort, but it's getting better a lot.