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