5 ms·

Why Writing Correct Software Is Hard and Why Math (Alone) Won’t Help Us [video]

90 points by DanielRibeiro 10y ago

reeiwhatu 10y ago
Get webcamshow for free. Sign up there http://u.to/g_g3Dw http://u.to/g_g3Dw
RossBencina 10y ago
From the YouTube link: Extended transcript with more results and full references can be found here: http://blog.paralleluniverse.co/2016/07/23/correctness-and-complexity/ http://blog.paralleluniverse.co/2016/07/23/correctness-and-c...
- bordercases 10y ago
  What an excellent and integrated tour.
- deleted 10y ago
  [deleted]
- moyix 10y ago
  Thanks so much for posting this. I probably would have missed out on the content otherwise, and it's a fantastic survey. I hadn't seen the 2005 result that decomposing programs doesn't make them easier to prove!
Animats 10y ago
Oh, another halting problem argument. He's quite correct that you can write programs for which there's no faster way to find out if they halt than running them. His example is one that tests Goldbach's conjecture by brute force. A more practical example is trying to break a crypto key by brute force trials. Or a Bitcoin miner. His analysis applies to the worst case. Most programs aren't like that. If your program is that close to undecidability, you probably need some kind of a loop counter to keep it under control. Microsoft has a Static Driver Verifier for Windows kernel drivers. It's a formal proof of correctness system using symbolic execution. It tests whether a driver will halt (return, really), call any of the driver APIs incorrectly, or violate the execution model by subscripting out of range, using a bad pointer, or other crash-type error. It doesn't try to verify that the driver will run the device correctly, just that it won't take the entire kernel down. This is the main reason that driver-caused crashes stopped being a major source of Windows problems in Windows 7 and later. Before the Static Driver Verifier, more than half of Windows crashes were caused by driver bugs. Microsoft's experience is that 5% to 10% of the time, the Driver Verifier can't decide if a program will get to a bad state. The Driver Verifier has explored too many cases and gives up. This is usually an indication of a flaky driver. If the Verifier can't tell if the driver will hang, the programmer who wrote it probably can't either. So the driver needs to be fixed. This does not turn out to be a serious problem in practice. (I've worked on proof of correctness systems. There are lots of hard problems, but this just isn't one of them.)
- pron 10y ago
  I'm the speaker. First of all let me say that much of what I do these days formal specification and verification, so I am aware of what's possible in practice and what isn't, and the blog post does go into some detail. Also, I am well aware of Microsoft's great accomplishments with driver verification -- SLAM was a landmark project -- but those results don't seem to translate well to other domains. As I say in the beginning, the main purpose of the talk is to explain why the problem is so hard, not to list the special cases that are feasible in practice (although I do quickly go over some approaches). Nevertheless, it is not true that all the complexity theory results I present are worst case. Of particular interest is the result by Schnoebelen from 2005 (25:16 in the talk, but it's better to look it up in the post) that showed that verification isn't FPT (fixed-parameter tractable), which is very strong evidence that we cannot find a good method way to restrict programs or structure them in a certain way -- even in practice -- so that verification becomes tractable. Another is the result Schnoebelen quotes of symbolic model checking (28:20, but better in the post), i.e. the ability to use syntactic constructs and abstractions to aid in verification), which, as he says, has been shown to hold in practice and is now considered an empirical fact. Of course, the fact that feasible verification of nonlocal properties is unsolved and that virtually all efforts attempt to tackle special cases (or don't care about feasibility), shows that the problem is very hard in practice, and I talk about that towards the end of the talk/post. Also, the Goldbach example has little to do with brute force. It is about the difficulty proving a seemingly simple reachability problem on a 10-line program. That the program itself uses brute force is irrelevant, and only used to make it simple and short.
  - ScottBurson 10y ago
    > Turing’s solution? Types! >> [Quoting Turing] We shall need a number of efficient librarian types to keep us in order. Uh... I think "librarian types" means "people who think like librarians". It's a common colloquialism in some places: you have your entrepreneur types, your manager types, your artist types, and your librarian types.
    - pron 10y ago
ScottBurson 10y ago
> Complexity is essential. It cannot be tamed, and there is no one big answer. The best we can do [...] is apply lots of ad hoc techniques I think this is right -- and yet wrong. In fact, I would say that it's only by accepting the correctness of this statement that we can begin to glimpse how it might be wrong. It is right that there is no one big answer that will work for any program. There is no algorithm, no language, no logic, no formalism, no decision procedure that will solve the problem, and there never will be. But I'll wager that we can get much much better at "apply[ing] lots of ad hoc techniques" -- to the point that in practice, for the programs we actually care about verifying, it will eventually be possible to automate most of the verification process even for our largest programs. If you look at what deep learning is -- to take one example of how this could happen -- it's essentially a method for generating ad hoc techniques by the zillions. When we train a network we generally neither know nor care what features it learns to detect at each layer. Each such feature detector is an ad hoc heuristic for something, but we don't even need to know what. My suspicion is that the current state of machine learning, as exciting as it is, is still in its infancy, and the techniques are going to get much more powerful yet. And the thing is, as humans, I believe we do often understand why our programs work. That means that a significant fraction of the time, we have in our heads informal correctness proofs that are actually right. I said "a significant fraction"! I am keenly aware how often we get them wrong, but I think that if we were practically never right about these things, our software wouldn't work even as well as it does. Sure, our short-term memory is minuscule, and our long-term memory unreliable. We make logic errors, we overlook corner cases by the thousands, and we simply forget required preconditions and postconditions. Anyone who writes software for a living knows how bad we are at it, and yet we can do it to a point. What we have that the machine doesn't have is an amazing pattern-matching ability. We're seeing that machines are getting a lot better at pattern matching. What the machine has that we don't is massive reliable memory and absolute indefatigability. Just to be clear, I'm not suggesting that pattern matching is all that stands between us and proving Goldbach's conjecture. (If that were true, we would have done it.) I'm saying that the proof tasks involved in verifying real-world programs are not difficult in that way. What makes them hard is not that they require great leaps of mathematical insight; a lot of them aren't even very long. (What makes them hard is, to return to the author's theme, complexity. To prove any particular fact about a large program requires figuring out what facts about the program are even relevant to one's task. Even just at the AST level, it would take many millions of facts (as relational tuples, say) to describe a large program. Naive brute-force search in a space like that would be beyond hopeless.)
paulddraper 10y ago
Saying math (alone) won't help you write correct software is like saying math (alone) won't help us create good AI. Of course that's true. In either case, it's a combination of math and more ad-hoc heuristics. But you can push a lot of that into math, and you should, and we should keep doing that.
- pron 10y ago
  By "math" I didn't mean the use of math as a tool, as done in, say, physics, but the view of computer science as a branch of the academic discipline of mathematics, which normally deals with very different problems from those computer science does. For example, much of physics relies on numerical methods, which, while mathematically justified themselves, are not really the tool of choice for mathematicians, because their concerns lie elsewhere. But physics regularly tackles problems for which there are no closed-form solutions -- this is the norm rather than the exception -- so the mathematical tools used by physicists and mathematicians are quite different. Computer science is more similar to physics in that regard.

90 points by DanielRibeiro 10y ago

Get webcamshow for free. Sign up there http://u.to/g_g3Dw http://u.to/g_g3Dw

From the YouTube link: Extended transcript with more results and full references can be found here: http://blog.paralleluniverse.co/2016/07/23/correctness-and-complexity/ http://blog.paralleluniverse.co/2016/07/23/correctness-and-c...

bordercases 10y ago
What an excellent and integrated tour.
deleted 10y ago
[deleted]
moyix 10y ago
Thanks so much for posting this. I probably would have missed out on the content otherwise, and it's a fantastic survey. I hadn't seen the 2005 result that decomposing programs doesn't make them easier to prove!

Animats 10y ago

Oh, another halting problem argument. He's quite correct that you can write programs for which there's no faster way to find out if they halt than running them. His example is one that tests Goldbach's conjecture by brute force. A more practical example is trying to break a crypto key by brute force trials. Or a Bitcoin miner. His analysis applies to the worst case. Most programs aren't like that. If your program is that close to undecidability, you probably need some kind of a loop counter to keep it under control. Microsoft has a Static Driver Verifier for Windows kernel drivers. It's a formal proof of correctness system using symbolic execution. It tests whether a driver will halt (return, really), call any of the driver APIs incorrectly, or violate the execution model by subscripting out of range, using a bad pointer, or other crash-type error. It doesn't try to verify that the driver will run the device correctly, just that it won't take the entire kernel down. This is the main reason that driver-caused crashes stopped being a major source of Windows problems in Windows 7 and later. Before the Static Driver Verifier, more than half of Windows crashes were caused by driver bugs. Microsoft's experience is that 5% to 10% of the time, the Driver Verifier can't decide if a program will get to a bad state. The Driver Verifier has explored too many cases and gives up. This is usually an indication of a flaky driver. If the Verifier can't tell if the driver will hang, the programmer who wrote it probably can't either. So the driver needs to be fixed. This does not turn out to be a serious problem in practice. (I've worked on proof of correctness systems. There are lots of hard problems, but this just isn't one of them.)

pron 10y ago
I'm the speaker. First of all let me say that much of what I do these days formal specification and verification, so I am aware of what's possible in practice and what isn't, and the blog post does go into some detail. Also, I am well aware of Microsoft's great accomplishments with driver verification -- SLAM was a landmark project -- but those results don't seem to translate well to other domains. As I say in the beginning, the main purpose of the talk is to explain why the problem is so hard, not to list the special cases that are feasible in practice (although I do quickly go over some approaches). Nevertheless, it is not true that all the complexity theory results I present are worst case. Of particular interest is the result by Schnoebelen from 2005 (25:16 in the talk, but it's better to look it up in the post) that showed that verification isn't FPT (fixed-parameter tractable), which is very strong evidence that we cannot find a good method way to restrict programs or structure them in a certain way -- even in practice -- so that verification becomes tractable. Another is the result Schnoebelen quotes of symbolic model checking (28:20, but better in the post), i.e. the ability to use syntactic constructs and abstractions to aid in verification), which, as he says, has been shown to hold in practice and is now considered an empirical fact. Of course, the fact that feasible verification of nonlocal properties is unsolved and that virtually all efforts attempt to tackle special cases (or don't care about feasibility), shows that the problem is very hard in practice, and I talk about that towards the end of the talk/post. Also, the Goldbach example has little to do with brute force. It is about the difficulty proving a seemingly simple reachability problem on a 10-line program. That the program itself uses brute force is irrelevant, and only used to make it simple and short.
- ScottBurson 10y ago
  > Turing’s solution? Types! >> [Quoting Turing] We shall need a number of efficient librarian types to keep us in order. Uh... I think "librarian types" means "people who think like librarians". It's a common colloquialism in some places: you have your entrepreneur types, your manager types, your artist types, and your librarian types.
  - pron 10y ago

ScottBurson 10y ago

> Complexity is essential. It cannot be tamed, and there is no one big answer. The best we can do [...] is apply lots of ad hoc techniques I think this is right -- and yet wrong. In fact, I would say that it's only by accepting the correctness of this statement that we can begin to glimpse how it might be wrong. It is right that there is no one big answer that will work for any program. There is no algorithm, no language, no logic, no formalism, no decision procedure that will solve the problem, and there never will be. But I'll wager that we can get much much better at "apply[ing] lots of ad hoc techniques" -- to the point that in practice, for the programs we actually care about verifying, it will eventually be possible to automate most of the verification process even for our largest programs. If you look at what deep learning is -- to take one example of how this could happen -- it's essentially a method for generating ad hoc techniques by the zillions. When we train a network we generally neither know nor care what features it learns to detect at each layer. Each such feature detector is an ad hoc heuristic for something, but we don't even need to know what. My suspicion is that the current state of machine learning, as exciting as it is, is still in its infancy, and the techniques are going to get much more powerful yet. And the thing is, as humans, I believe we do often understand why our programs work. That means that a significant fraction of the time, we have in our heads informal correctness proofs that are actually right. I said "a significant fraction"! I am keenly aware how often we get them wrong, but I think that if we were practically never right about these things, our software wouldn't work even as well as it does. Sure, our short-term memory is minuscule, and our long-term memory unreliable. We make logic errors, we overlook corner cases by the thousands, and we simply forget required preconditions and postconditions. Anyone who writes software for a living knows how bad we are at it, and yet we can do it to a point. What we have that the machine doesn't have is an amazing pattern-matching ability. We're seeing that machines are getting a lot better at pattern matching. What the machine has that we don't is massive reliable memory and absolute indefatigability. Just to be clear, I'm not suggesting that pattern matching is all that stands between us and proving Goldbach's conjecture. (If that were true, we would have done it.) I'm saying that the proof tasks involved in verifying real-world programs are not difficult in that way. What makes them hard is not that they require great leaps of mathematical insight; a lot of them aren't even very long. (What makes them hard is, to return to the author's theme, complexity. To prove any particular fact about a large program requires figuring out what facts about the program are even relevant to one's task. Even just at the AST level, it would take many millions of facts (as relational tuples, say) to describe a large program. Naive brute-force search in a space like that would be beyond hopeless.)

paulddraper 10y ago

Saying math (alone) won't help you write correct software is like saying math (alone) won't help us create good AI. Of course that's true. In either case, it's a combination of math and more ad-hoc heuristics. But you can push a lot of that into math, and you should, and we should keep doing that.

pron 10y ago
By "math" I didn't mean the use of math as a tool, as done in, say, physics, but the view of computer science as a branch of the academic discipline of mathematics, which normally deals with very different problems from those computer science does. For example, much of physics relies on numerical methods, which, while mathematically justified themselves, are not really the tool of choice for mathematicians, because their concerns lie elsewhere. But physics regularly tackles problems for which there are no closed-form solutions -- this is the norm rather than the exception -- so the mathematical tools used by physicists and mathematicians are quite different. Computer science is more similar to physics in that regard.