6 ms·

Formal Reasoning About Programs (2017) [pdf]

83 points by p0llard 7y ago

DoofusOfDeath 7y ago
The link provided seems down (hug of death?) I'm guessing that this is the same material: https://github.com/achlipala/frap https://github.com/achlipala/frap
- philzook 7y ago
  Seems up to me.
- nextos 7y ago
  Try http://adam.chlipala.net/frap/ http://adam.chlipala.net/frap/ It's a really great book as an introduction to semantics and proofs. A great alternative is http://www.concrete-semantics.org/ http://www.concrete-semantics.org/. Concrete Semantics uses Isabelle, which is based on ZFC set theory. Whereas FRAP uses Coq, that employs constructive types. https://softwarefoundations.cis.upenn.edu https://softwarefoundations.cis.upenn.edu is also fantastic, covers some of the same topics, and proceeds a bit more slowly. I'm betting formal methods will become more wildly used in the 2020s. It'd be interesting to see e.g. reinforcement learning used to automate proof discovery.
  - crimsonalucard 7y ago
    >I'm betting formal methods will become more wildly used in the 2020s. It'd be interesting to see e.g. reinforcement learning used to automate proof discovery. Even though I think formal methods in programming would be a great thing, If anything I see evidence for it not happening. I got hired into a new job last year and I mentioned it as one of my interests and the guy literally laughed in my face commenting at how pointless it is proving a program to be correct. What is it that makes you think formal methods will become more popular?
    - DoofusOfDeath 7y ago
      Sadly, I share your pessimism about formal methods. I suspect one of the headwinds is that there's a greater demand for more software than there is for better-proven software.
      - tuvistavie 7y ago
        At the end of the day I think it's just a matter of cost. If it's cheaper to let a software fail and simply fix it when it does, there will not be much interest into proving it to be correct. If a failure will likely be vastly more expensive than proving correctness, then proving correctness will make sense. There are simply way less instances of the second category. I think one of the few "new" instances, which might be worth mentioning is smart contract programming, where failures can cause millions of loss and proving correctness is not too expensive.
        crimsonalucard 7y ago
        With the amount of infrastructure focused around testing I think the opposite is true. I think it's more ignorance and culture. Many people don't know about formal methods.
        Ididntdothis 7y ago
        Agreed.
      - zozbot234 7y ago
        Having better-proven software is a precondition to having more software. Especially if you expect that things like program synthesis are going to be increasingly important - who wants to "synthesize" buggy code?
    - lmeyerov 7y ago
      I'm super bullish, but for a bit further out and for a different reason than the vast bulk of PL folks: a major value jump in AI. The current wave of ML techniques are approaching a plateau. The current approach is use deep learning, then iterate by adding fancier models / more data / more compute. That loop has diminishing returns on time/$ spent, so it's now time for the next big value jump, similar to when DL models started to relatively easily outperform Bayesian models on certain problems. Interestingly, both the problem domain of what to solve, and how fancy solutions work, increasingly looks a lot like programs. Relational learning, automation, ... A growing subfield in the proof world is Program Synthesis, which looks at all sorts of techniques to do just that. Two lessons from there has been proof solvers can get you quite far, and increasingly, that you can combine traditional logic solvers with ML techniques to great benefit. If I was OpenAI, I'd take Microsoft's $1B and spend less on running bigger models and people doing incremental tweaks to them and a LOT on people working here. (I do think proofs-for-programs also has bigger adoption hopes in areas like security, but that's a much more nuanced and domain-specific story. Meanwhile, we do see continued niche success for more niche NASA and DoD style work, so the small money train will continue driving the community's focus on stuff like OS verification.)
rovolo 7y ago
This book and the Coq proof assistant are what pushed me to learn Emacs. The 'coqide' application my class (CSE 505 at UW) used was not a good text editing experience. Emacs + Proof General by contrast were incredible. It's important to have a solid on-ramp for beginners. I tried using Emacs for a Java project in my next class, but I never managed to set up anything as nice as the IntelliJ IDE. I'm sure setting up something nicer is possible, but first impressions matter.
- jakear 7y ago
  There’s also a nice VS Code extension for Coq I used when taking Adam’s class.

83 points by p0llard 7y ago

The link provided seems down (hug of death?) I'm guessing that this is the same material: https://github.com/achlipala/frap https://github.com/achlipala/frap

philzook 7y ago
Seems up to me.
nextos 7y ago
Try http://adam.chlipala.net/frap/ http://adam.chlipala.net/frap/ It's a really great book as an introduction to semantics and proofs. A great alternative is http://www.concrete-semantics.org/ http://www.concrete-semantics.org/. Concrete Semantics uses Isabelle, which is based on ZFC set theory. Whereas FRAP uses Coq, that employs constructive types. https://softwarefoundations.cis.upenn.edu https://softwarefoundations.cis.upenn.edu is also fantastic, covers some of the same topics, and proceeds a bit more slowly. I'm betting formal methods will become more wildly used in the 2020s. It'd be interesting to see e.g. reinforcement learning used to automate proof discovery.
- crimsonalucard 7y ago
  >I'm betting formal methods will become more wildly used in the 2020s. It'd be interesting to see e.g. reinforcement learning used to automate proof discovery. Even though I think formal methods in programming would be a great thing, If anything I see evidence for it not happening. I got hired into a new job last year and I mentioned it as one of my interests and the guy literally laughed in my face commenting at how pointless it is proving a program to be correct. What is it that makes you think formal methods will become more popular?
  - DoofusOfDeath 7y ago
    Sadly, I share your pessimism about formal methods. I suspect one of the headwinds is that there's a greater demand for more software than there is for better-proven software.
    - tuvistavie 7y ago
      At the end of the day I think it's just a matter of cost. If it's cheaper to let a software fail and simply fix it when it does, there will not be much interest into proving it to be correct. If a failure will likely be vastly more expensive than proving correctness, then proving correctness will make sense. There are simply way less instances of the second category. I think one of the few "new" instances, which might be worth mentioning is smart contract programming, where failures can cause millions of loss and proving correctness is not too expensive.
      - crimsonalucard 7y ago
        With the amount of infrastructure focused around testing I think the opposite is true. I think it's more ignorance and culture. Many people don't know about formal methods.
        Ididntdothis 7y ago
        Agreed.
    - zozbot234 7y ago
      Having better-proven software is a precondition to having more software. Especially if you expect that things like program synthesis are going to be increasingly important - who wants to "synthesize" buggy code?
  - lmeyerov 7y ago
    I'm super bullish, but for a bit further out and for a different reason than the vast bulk of PL folks: a major value jump in AI. The current wave of ML techniques are approaching a plateau. The current approach is use deep learning, then iterate by adding fancier models / more data / more compute. That loop has diminishing returns on time/$ spent, so it's now time for the next big value jump, similar to when DL models started to relatively easily outperform Bayesian models on certain problems. Interestingly, both the problem domain of what to solve, and how fancy solutions work, increasingly looks a lot like programs. Relational learning, automation, ... A growing subfield in the proof world is Program Synthesis, which looks at all sorts of techniques to do just that. Two lessons from there has been proof solvers can get you quite far, and increasingly, that you can combine traditional logic solvers with ML techniques to great benefit. If I was OpenAI, I'd take Microsoft's $1B and spend less on running bigger models and people doing incremental tweaks to them and a LOT on people working here. (I do think proofs-for-programs also has bigger adoption hopes in areas like security, but that's a much more nuanced and domain-specific story. Meanwhile, we do see continued niche success for more niche NASA and DoD style work, so the small money train will continue driving the community's focus on stuff like OS verification.)

rovolo 7y ago

This book and the Coq proof assistant are what pushed me to learn Emacs. The 'coqide' application my class (CSE 505 at UW) used was not a good text editing experience. Emacs + Proof General by contrast were incredible. It's important to have a solid on-ramp for beginners. I tried using Emacs for a Java project in my next class, but I never managed to set up anything as nice as the IntelliJ IDE. I'm sure setting up something nicer is possible, but first impressions matter.

jakear 7y ago
There’s also a nice VS Code extension for Coq I used when taking Adam’s class.