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.
FWIW, I'm not mathematically-inclined and haven't found Coq to be painful to use. As soon as I really want verified code, doing stuff in Coq seems like the easiest path because the proof automation tooling is pretty great, especially if you follow the approach in Certified Programming with Dependent Types[0].
I also like Alloy[1] for messing around with logical data structure definitions interactively.
Hey, I was at that same school. What I also liked about F* is the ACL2 feel. Compared to Coq for instance, F* feels more like "my program proves itself" than "I'm writing a proof of my program".
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).
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.
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).
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.
[+] [-] wk_end|10 years ago|reply
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.
[+] [-] erichocean|10 years ago|reply
I also like Alloy[1] for messing around with logical data structure definitions interactively.
[0] http://adam.chlipala.net/cpdt/
[1] http://alloy.mit.edu/alloy/
[+] [-] p4bl0|10 years ago|reply
[+] [-] MichaelBurge|10 years ago|reply
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.
[+] [-] iheartmemcache|10 years ago|reply
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).
[+] [-] pron|10 years ago|reply
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.
[+] [-] chriswarbo|10 years ago|reply
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 ;)
[+] [-] tom_mellior|10 years ago|reply
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.
[+] [-] Avshalom|10 years ago|reply
https://en.wikipedia.org/wiki/Altran_Praxis
[+] [-] throwaway999888|10 years ago|reply
[+] [-] tom_mellior|10 years ago|reply
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.
[+] [-] platz|10 years ago|reply
[+] [-] unknown|10 years ago|reply
[deleted]