Verified Programming in F*: A Tutorial(fstar-lang.org)
fstar-lang.org
Verified Programming in F*: A Tutorial
http://www.fstar-lang.org/tutorial/
5 comments
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.
[0] http://adam.chlipala.net/cpdt/
[1] http://alloy.mit.edu/alloy/
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/
I think the pain only appears when you start trying to do "deep specification" of large systems. My research group has about 5-10 of us that have all built large systems (5-60 kloc) and verified them in Coq. I know each of us long list of gripes with the tooling.
My recent work has been on a verified JIT compiler and having to write tactics and lemmas to deal with facts about bit vectors seems stupid when SMT solvers are particularly good at this kind of reasoning.
My recent work has been on a verified JIT compiler and having to write tactics and lemmas to deal with facts about bit vectors seems stupid when SMT solvers are particularly good at this kind of reasoning.
When you say that you verified a large system in Coq, in what language did you write your system? does it mean that your language semantics has do be defined in Coq, or did you write your system using Coq as a programming language?
I'm with you that, depending on the problem, different verification approaches make the most sense. I wish it was easier to combine results from different tooling.
I thought about trying Alloy since in not mathematical enough for HOL, etc. An EAL7 VPN project used it too, IIRC. Do you have a link to a tutorial or reference for how you apply it to data structure def's?
I use the visualizer and just worked through the examples and tutorials on the Alloy website. It takes a little bit to get used to, but the visualizations really help to see what's going on.
What I like Alloy for is checking to see if the operations you're defining to maintain a data structure actually maintain the desired invariants. It's nice for situations where you're not actually sure that what you're "trying to do" will even work like you expect.
With Coq, I tend to already know something will work and just want to verify that I've achieved it, so it's much less exploratory in nature.
What I like Alloy for is checking to see if the operations you're defining to maintain a data structure actually maintain the desired invariants. It's nice for situations where you're not actually sure that what you're "trying to do" will even work like you expect.
With Coq, I tend to already know something will work and just want to verify that I've achieved it, so it's much less exploratory in nature.
Ok. That makes a little more sense. I'll just have to remember to use the visualizer if I get time to try it.
Another interesting tool is ProB[1]. I believe it does symbolic model checking and supports partial order reduction. It works on specifications in multiple languages, including TLA+, but I haven't had the chance to use it myself because it doesn't support all TLA+ features. In particular, it doesn't support TLA+'s higher-order operators, which my specifications use.
[1]: Cool visualizations: https://www3.hhu.de/stups/prob/index.php/State_space_visuali...
[1]: Cool visualizations: https://www3.hhu.de/stups/prob/index.php/State_space_visuali...
Appreciate the reference. I'm holding off on ProB and B for now because the B method has mixed results in CompSci literature. I mean, it's been proven on a number of high assurance projects by pro's. I at least like that both B and TLA+ are pretty straight-forward to compared to most where a person has both a mathematical and good, mental model of what's going on. B particularly as it maps to imperative with ease.
I'm keeping it bookmarked just in case. Meanwhile, I just got a ton of stuff on asynchronous verification in response to another commenter's troubles there. I was away too long: looks like async and GALS are both mostly solved problems at the cutting edge with some tools to help. A lot to skim or read that puts my B experiments further on the backlog.
I'm keeping it bookmarked just in case. Meanwhile, I just got a ton of stuff on asynchronous verification in response to another commenter's troubles there. I was away too long: looks like async and GALS are both mostly solved problems at the cutting edge with some tools to help. A lot to skim or read that puts my B experiments further on the backlog.
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.
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).
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).
> it's not Google, Facebook, or Apple that's the Bell Labs of our generation - it's Microsoft
That is quite true, the amount of research they put out in OS, programming languages and distributed systems is quite impressive.
They are the ones that have invested more in doing OSes in more safer programming languages or tooling.
Also many don't realize how quite a few main contributors of their beloved open source languages are actually on MSR payroll.
That is quite true, the amount of research they put out in OS, programming languages and distributed systems is quite impressive.
They are the ones that have invested more in doing OSes in more safer programming languages or tooling.
Also many don't realize how quite a few main contributors of their beloved open source languages are actually on MSR payroll.
> The military, aerospace industry and once in a while the medical industry will require provable code.
Not in the US... but in France, sure.
Not in the US... but in France, sure.
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.
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.
upandabout(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 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 ;)
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.
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.
https://en.wikipedia.org/wiki/Altran_Praxis
https://en.wikipedia.org/wiki/Altran_Praxis
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.
[1] http://www.spark-2014.org/contributors
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.
[1] http://www.spark-2014.org/contributors
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.
The closest to what you want might be ATS.
Thanks for the suggestion - ATS does look interesting and I hadn't heard of it before.
I wrote some posts on using ATS and interfacing with C if you want to dig further into it https://bluishcoder.co.nz/tags/ats/
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.
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.
[deleted]
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.