Who hires people to work in theorem provers, or using languages allowing proofs alongside code? I've always wanted to use them as a tool alongside unit tests or randomized testing, but they require dedicated language support so I haven't had the chance to test it on any 'real' code[1].
Is there a good language with the simplicity, portability, and control of C together with theorem-proving features? Like if I'm writing a memory allocator or something, I'd want to keep cache in mind, control when I ask the kernel for more pages, try not to fragment the heap, compile to simple assembly code so that there aren't expensive context switches, etc. But it'd also be nice to carry along a proof that the heap doesn't get fragmented in a certain way.
[1] An example of 'unreal' code would be me spending a weekend trying to write Goodstein's Theorem in Coq. 'Real' code would be a web app written in Perl.
> Who hires people to work in theorem provers, or using languages allowing proofs alongside code?
The military, aerospace industry and once in a while the medical industry will require provable code. Certain components need to be validated by frameworks like SPARK written in Ada. F* and Idris are pretty close to real-world usable in the capacity you're referring to. Those and ATS are probably the most 'real world' other than Ada/Spark. Other than that it's mostly universities and research facilities.
Another Microsoft Research project (I've said it once, I'm going to say it a million times more - hate on them all you want - it's not Google, Facebook, or Apple that's the Bell Labs of our generation - it's Microsoft) has a formal C verifier[1] which is paired in Z3, but I'm not sure if you could enforce an invariant like ensuring only a certain type of memory fragmentation. This Microsoft Research paper[2] strangely enough might be relevant re: memory alloc guarantees.
Other than that,'who hires people' ? Universities (INRIA of OCaml/Coq/Smalltalk Pharo fame probably at the forefront, that Swiss uni likely second edit: ETH Zurich is apparently ranked significantly higher than Jusseiu, mea culpa) Institutions like the Max Planck and Microsoft Research, Cambridge UK tend to hire people in a purely research-for-the-sake-of-research capacity which is exceedingly rare in the climate of only-think-about-this-quarters-profitability. I think JetBrains was doing some work with MPS that was really interesting though not quite in the vein of formal verification.
[1] https://vcc.codeplex.com/
[2] A Precise Yet Efficient Memory Model For C. Ernie Cohen, Michał Moskal, Wolfram Schulte, Stephan Tobies. 4th International Workshop on Systems Software Verification (SSV2009).
Good answers. I think Microsoft has tools that integrate into C# like tgey used for VerveOS. Coq extracts to ML's that could be converted to F# probably. So, even they have options that were practical enough for both an OS and their hypervisor.
I know Amazon, Microsoft and Oracle routinely use TLA+, as do many smaller companies. TLA+ is a specification language that includes both a model checker and a theorem prover, and the companies I mentioned use TLA+ tp specify and formally verify real-world code (e.g. Amazon uses it to specify and verify most of the AWS services; Intel uses it to verify chip design).
In practice, the theorem prover is not used much in real-world applications because proofs are very, very expensive[1], but the model checker is used very often and I've found it to be extremely useful.
[1]: seL4 required 30 man-years to prove a <10KLOC C program. The cost of proofs may grow exponentially in the size of the codebase.
> An example of 'unreal' code would be me spending a weekend trying to write Goodstein's Theorem in Coq. 'Real' code would be a web app written in Perl.
I doubt that "web app written in Perl" will be a realistic target for provably-correct code in, say, the next decade. It's much more likely that, as the cost of verification decreases, critical components will start becoming verified. For example, the core routines of encryption libraries, network schedulers, payment systems, etc.
Even so, some properties (e.g. memory safety) can be proven at the language level. That way, by verifying a Perl interpreter, we automatically verify every "web app written in Perl" for free ;)
> Is there a good language with the simplicity, portability, and control of C together with theorem-proving features?
Yes: C ;-) The Frama-C system allows you to write functional specifications of C code and verify them. Trivial example: http://frama-c.com/wp.html
It interfaces with the Why3 platform, which means that it can talk to dozens of automated provers out of the box. AFAIK it doesn't yet handle some things like dynamic allocation and free (the semantics of free in C is hard!), but it may be something you might want to play with.
I've got no idea what they do now but Altran UK nee Praxis was mildly (in)famous for using formal methods and verifiable code. The Paris Metro I think is the notable one they did, something with French trains at the least.
Altran is a major contributor to SPARK these days [1].
I've been a big believer in TDD for many years (and still am), but reading a lot of Dijkstra lately I started to feel guilty for not keeping up with the state of the art in formal techniques. :) So I've been looking around in just the last couple of weeks to figure out what the best tools are these days. This discussion has been very helpful.
Anyone wanting to see their Correct by Construction method in action can Google Tokeneer. It was a demo sponsored by NSA and open sourced to inspire more companies to write tobust software that could meet EAL5 at least. Simple enough for beginners go understand too.
Is there a good language with the simplicity, portability, and control of C together with theorem-proving features? Like if I'm writing a memory allocator or something, I'd want to keep cache in mind, control when I ask the kernel for more pages, try not to fragment the heap, compile to simple assembly code so that there aren't expensive context switches, etc. But it'd also be nice to carry along a proof that the heap doesn't get fragmented in a certain way.
[1] An example of 'unreal' code would be me spending a weekend trying to write Goodstein's Theorem in Coq. 'Real' code would be a web app written in Perl.