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.
I was initially excited about this; a prover with a logic like Coq (dependent types!) but with awesome extensions (effects!) and with the automation of Z3 seems pretty neat. I decided to test-drive it with the first few chapters of the Software Foundations book (https://www.cis.upenn.edu/~bcpierce/sf/current/index.html).
Now, I must admit, I'm a lot less excited :-( You can see my results for (almost all of) the first two chapters here: http://pastebin.com/5bL7Wugq http://pastebin.com/GRFLCF8Z
Unfortunately, proving in F* turned out to be a pain. The basic problem is that during proving you have no idea at all about the state of the proof; the only way I could get anything done when automation failed (and that was more often than I had hoped) was by working out, in comments, a very detailed proof, and then applying appropriate lemmas. If you know Coq, think of it as writing down tactics without seeing the proof state in the side pane, and having to get it complete before you get a simple yes/no answer telling you whether what you did was good enough to make the entire proof go through. But in fact, it it is even more painful than that: In Coq, you can apply/rewrite with lemmas just by naming them, but in F* you need to instantiate all arguments. So a proof step for one of the lemmas in the second document above, which would be rewrite -> plus_swap in Coq, in F* must be written plus_swap n m' (mult (S n) m') although Z3 could easily find the correct arguments itself. But leaving arguments off is simply not possible in a system of this kind based on the notion that a "proof" is written a well-typed program.
Oh well. Back to Isabelle/HOL for my regular theorem proving needs, although its logic is really weird and I wish there was some system combining the automation of Isabelle with the Calculus of Constructions.
F* would be useful in the same way Liquid Haskell would be useful.
I got to try F* with the developers maybe a year ago at a school in Paris. It's an amazing language when the SMT solver Just Works, but both I and the other students I spoke with were very frustrated when it didn't. Aside from the lack of Coq-style tactics, IIRC Z3 didn't give much feedback about why it couldn't prove something; when things don't work, you kind of just had to plug away awkwardly writing lemmas until Z3 can figure out what you want to prove.
That being said, this document seems to now mention something about experimental support for automatic induction, which (again, IIRC) we didn't have a year ago in Paris, so maybe that'll help. If the F* team can get over the last few hurdles and make using it ever so slightly smoother I honestly think it'll be a real game-changer: their approach to refinement types give you a tremendous degree of statically-enforced correctness without the pain of more academic dependently typed theorem provers like Coq or Agda.