| > Human intuition does consistently do better than automated tools, but there is no single easily recognizable "trick" or "method" to it, which makes it hard to implement in a tool. Except in software verification, the facts on the ground are that it is the automated tools that do better than humans. We're not talking hypotheticals or speculation here. If you've written software proofs you won't find this particularly surprising. They're tedious and frustrating, but rarely require much ingenuity. Attention to detail plays a far more important role [1]. They're not at all like proving mathematical theorems. Software proofs are to math proofs what painting a hospital is to painting the Sistine Chapel. > In my view, the reason that theoretical results do not apply very directly to human reasoning is precisely that human reasoning is "intuitive" and hard to capture in a program. Perhaps, but so far humans do not seem to outperform the expectations. So you're counting on a human ability that, to date, we've not seen. In fact, humans rarely if ever beat computational complexity expectations. SAT solvers do much better than humans at supposedly-NP-complete problems, for example, and so do various approximation algorithms. Why doesn't our intuition help us outperform algorithms there? And again, if intuition were the decisive factor, how come we're doing such a terrible job? If algorithms beat us today, what kind of boost in intuition do you expect that will allow us to beat them tomorrow? Look, formal proofs are great. They're clearly the gold standard. So I encourage everyone here who thinks proofs are the future of software correctness to try them out to write correct large and complex programs. The problem is that they'll fail, and either abandon formal methods altogether, or worse, waste their time proving what they can at the expense of verifying what they should. > but if you want to be able to use the full power of human intuition, instead of restricting yourself to program properties that are easy to prove automatically, then there is no way around manual proofs. Maybe. It's certainly possible that one day we'll figure out how to make manual proofs work reasonably well for software verification. It's also possible that by then automated tools will get even better, especially considering that, as they've shown greater promise over the past few decades, that's where most of the research is focused. Sure, there will always be some niches where tedious manual work is required, but I see no indication that that niche would grow beyond the size it occupies now, an important yet small part of formal verification. [1]: https://brooker.co.za/blog/2014/03/08/model-checking.html |