> 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.
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).