That's pretty neat. I like seeing exotic languages used in mainstream projects. It's just fun, ya know? Firefox is also shipping with some Rust code these days.
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.
Now amazon is trying to formally verify a lot of AWS with TLA+ and other techniques. Here Mozilla is trying to verify it’s crypto.
Given the increasing rise of cyber security problems and their consequences, will formal verifications once again become more standard in software engineering? At minimum, we’ll need to see more user-friendly variants of TLA+ and other techniques for average developers to be able to use. Probably it should be taught in normal CS education. Even better would be for some kind of AI to help take existing code or specs and put it into something that can be formally proved.
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.
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.
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.
Bravo! Looking forward to that.
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.