7 ms·

Verified Programming in F*: A Tutorial

95 points by namin 11y ago

wk_end 11y ago
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.
- erichocean 11y ago
  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/ http://adam.chlipala.net/cpdt/ [1] http://alloy.mit.edu/alloy/ http://alloy.mit.edu/alloy/
  - nickpsecurity 11y ago
    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?
    - pron 11y ago
      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_visualization_examples https://www3.hhu.de/stups/prob/index.php/State_space_visuali...
      - nickpsecurity 11y ago
        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.
    - erichocean 11y ago
      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.
      - nickpsecurity 11y ago
        Ok. That makes a little more sense. I'll just have to remember to use the visualizer if I get time to try it.
  - jroesch 11y ago
    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.
    - yodsanklai 11y ago
      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?
    - erichocean 11y ago
      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.
- p4bl0 11y ago
  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".
MichaelBurge 11y ago
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.
- throwaway999888 11y ago
  The closest to what you want might be ATS.
  - MichaelBurge 11y ago
    Thanks for the suggestion - ATS does look interesting and I hadn't heard of it before.
    - doublec 11y ago
      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/ https://bluishcoder.co.nz/tags/ats/
- iheartmemcache 11y ago
  > 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/ 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).
deleted 11y ago
[deleted]
platz 11y ago
F* would be useful in the same way Liquid Haskell would be useful.
tom_mellior 11y ago
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 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/5bL7Wugq http://pastebin.com/GRFLCF8Z 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.

95 points by namin 11y ago

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.

erichocean 11y ago
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/ http://adam.chlipala.net/cpdt/ [1] http://alloy.mit.edu/alloy/ http://alloy.mit.edu/alloy/
- nickpsecurity 11y ago
  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?
  - pron 11y ago
    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_visualization_examples https://www3.hhu.de/stups/prob/index.php/State_space_visuali...
    - nickpsecurity 11y ago
      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.
  - erichocean 11y ago
    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.
    - nickpsecurity 11y ago
      Ok. That makes a little more sense. I'll just have to remember to use the visualizer if I get time to try it.
- jroesch 11y ago
  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.
  - yodsanklai 11y ago
    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?
  - erichocean 11y ago
    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.
p4bl0 11y ago
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".

MichaelBurge 11y ago

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.

throwaway999888 11y ago
The closest to what you want might be ATS.
- MichaelBurge 11y ago
  Thanks for the suggestion - ATS does look interesting and I hadn't heard of it before.
  - doublec 11y ago
    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/ https://bluishcoder.co.nz/tags/ats/
iheartmemcache 11y ago
> 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/ 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).

deleted 11y ago

[deleted]

platz 11y ago

F* would be useful in the same way Liquid Haskell would be useful.

tom_mellior 11y ago

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 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/5bL7Wugq http://pastebin.com/GRFLCF8Z 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.