Formal Reasoning About Programs (2017) [pdf](adam.chlipala.net)
adam.chlipala.net
Formal Reasoning About Programs (2017) [pdf]
http://adam.chlipala.net/frap/frap_book.pdf
23 comments
Try 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/.
Concrete Semantics uses Isabelle, which is based on ZFC set theory. Whereas FRAP uses Coq, that employs constructive types.
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.
It's a really great book as an introduction to semantics and proofs.
A great alternative is 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 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.
>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?
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?
> ”What is it that makes you think formal methods will become more popular?”
Well, we’re hiring those skills into one of the world’s larger banks. As are peers with similar industry challenges.
Well, we’re hiring those skills into one of the world’s larger banks. As are peers with similar industry challenges.
Really? You have a software engineering job where a required skill set is formal methods? That's interesting. What is the role and how do they use it?
Yes, I had such roles available at both my last job and this one where I am actively hiring senior/staff/principal engineers who can contribute.
See early basics in "Bridgewater Associates discuss the use of ARG tools at AWS Summit in NYC" shared here:
https://www.youtube.com/watch?v=gJhV35-QBE8
For slides, try "The Theory and Math Behind Data Privacy and Security Assurance (SEC301) - AWS re:Invent 2018" here:
https://www.slideshare.net/AmazonWebServices/the-theory-and-...
A few more public links about what's going on in the field here:
http://www0.cs.ucl.ac.uk/staff/b.cook/ARG.html
A more enterprisey collection:
https://aws.amazon.com/security/provable-security/
Please recognize that most of what we'd like to talk about, we can't. It's difficult for folks doing this kind of work to get clearance to talk about it. But more are undertaking this than you might think. Drop me a note if interested.
See early basics in "Bridgewater Associates discuss the use of ARG tools at AWS Summit in NYC" shared here:
https://www.youtube.com/watch?v=gJhV35-QBE8
For slides, try "The Theory and Math Behind Data Privacy and Security Assurance (SEC301) - AWS re:Invent 2018" here:
https://www.slideshare.net/AmazonWebServices/the-theory-and-...
A few more public links about what's going on in the field here:
http://www0.cs.ucl.ac.uk/staff/b.cook/ARG.html
A more enterprisey collection:
https://aws.amazon.com/security/provable-security/
Please recognize that most of what we'd like to talk about, we can't. It's difficult for folks doing this kind of work to get clearance to talk about it. But more are undertaking this than you might think. Drop me a note if interested.
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.
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.
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.
I think it's more ignorance and culture. Many people don't know about formal methods.
Agreed.
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?
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.)
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.)
> What is it that makes you think formal methods will become more popular?
I have an MSc where I focused in formal methods and I worked pretty extensively with them both in academia and industry before moving to machine learning, getting another MSc and a PhD.
There are many formal methods industrial users, especially those dealing with hardware and safety critical systems. For them, the cost / benefit ratio of using formal methods makes a lot of sense.
My hope is that lightweight approaches become more polished and it becomes feasible to use them in more mainstream applications. There is a whole range of methods going from type and effect systems, model checking, data and control flow analysis all the way to abstract interpretation and theorem proving. For example, refinement types as implemented in Liquid Haskell are a nice promising area.
I also think there are potentially very interesting combinations of deep learning and probabilistic inference plus formal methods that might push both AI and software engineering further. For example, an intelligent agent that is trying to infer (synthesize or induce) a program that models some function [1] might be able to carry a much better search by using abstract interpretation.
[1] https://www.sas.upenn.edu/~astocker/lab/teaching-files/PSYC7...
I have an MSc where I focused in formal methods and I worked pretty extensively with them both in academia and industry before moving to machine learning, getting another MSc and a PhD.
There are many formal methods industrial users, especially those dealing with hardware and safety critical systems. For them, the cost / benefit ratio of using formal methods makes a lot of sense.
My hope is that lightweight approaches become more polished and it becomes feasible to use them in more mainstream applications. There is a whole range of methods going from type and effect systems, model checking, data and control flow analysis all the way to abstract interpretation and theorem proving. For example, refinement types as implemented in Liquid Haskell are a nice promising area.
I also think there are potentially very interesting combinations of deep learning and probabilistic inference plus formal methods that might push both AI and software engineering further. For example, an intelligent agent that is trying to infer (synthesize or induce) a program that models some function [1] might be able to carry a much better search by using abstract interpretation.
[1] https://www.sas.upenn.edu/~astocker/lab/teaching-files/PSYC7...
> There is a whole range of methods going from type and effect systems, model checking, data and control flow analysis all the way to abstract interpretation and theorem proving.
I've seen some informal claims that many of these methods/approaches can be rephrased as special cases of abstract interpretation. This suggests that people who just focus on the multitude of "methods" out there might be missing something important about the "big picture" in the field.
I've seen some informal claims that many of these methods/approaches can be rephrased as special cases of abstract interpretation. This suggests that people who just focus on the multitude of "methods" out there might be missing something important about the "big picture" in the field.
All of them can be rephrased as special cases of abstract interpretation, but that observation doesn't really help you develop them or implement them efficiently.
I would think that once formal methods become easier to use they will be super useful. I am pretty sure 10 or 20 years they would have laughed at you if you had talked about automated testing on the scale we do now.
I used to work for a chip company. For the first 10 or so years I was there formal methods were 'some time in the future' However a year or so before I left (in 2013) a formal tool called Jasper popped up that was really productive in silicon verification (that is, testing/QA, but taken really seriously). It didn't cover everything - sometimes it got stuck and you had to test that case the old way. But it did a lot of work.
The tool could do formal proofs, although when I left it wasn't used in the way theorem-prover people seem to imagine them being used: starting by a full model of what the workpiece should do. Instead, it was used to prove assertions were always/never true. But in HW we have a lot of assertions :-)
For software there are a couple of issues: one is that the state is a lot bigger (in theory of course HW state is a superset of SW state, but in practice the content of most RAM can be regarded as just content and you don't need to prove anything about it other than that it is copied okay).
The other is that with the skimpy amount of testing most teams do, there isn't a huge pressure to find a way to reduce testing costs like there is in HW (where 2 engineers writing tests to one writing verilog isn't unusual).
The tool could do formal proofs, although when I left it wasn't used in the way theorem-prover people seem to imagine them being used: starting by a full model of what the workpiece should do. Instead, it was used to prove assertions were always/never true. But in HW we have a lot of assertions :-)
For software there are a couple of issues: one is that the state is a lot bigger (in theory of course HW state is a superset of SW state, but in practice the content of most RAM can be regarded as just content and you don't need to prove anything about it other than that it is copied okay).
The other is that with the skimpy amount of testing most teams do, there isn't a huge pressure to find a way to reduce testing costs like there is in HW (where 2 engineers writing tests to one writing verilog isn't unusual).
Type systems are getting more interesting as time goes on as innovations from research and niche languages are making it into the mainstream. A particularly interesting one to me is dependent types. That's where you can start to prove more interesting things about your code. It's juuuust beginning to make its way into practical use. I'd expect once that happens, we might see a gradual transition towards proving more and more invariants and properties of your code.
The curry lambek howard isomorphism has been known for a while. Coq, the language that is used by the posted textbook is a dependently typed language and was released 30 years ago.
Nobody builds web servers in Coq, but they do in Haskell, which I believe has some form dependent types coming. That's the kind of moving from niche languages to increasingly mainstream ones I mean. From there, maybe eventually it gets refined and even later properly mainstream.
Sorta, but not precisely. But it's the kind of progress I see as encouraging for the future of formal methods in mainstream software development.
Sorta, but not precisely. But it's the kind of progress I see as encouraging for the future of formal methods in mainstream software development.
Seems up to me.
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.
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.
There’s also a nice VS Code extension for Coq I used when taking Adam’s class.
I'm guessing that this is the same material: https://github.com/achlipala/frap