Why Writing Correct Software Is Hard and Why Math (Alone) Won’t Help Us [video]
&gt; 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<p>I think this is right -- and yet wrong.  In fact, I would say that it&#x27;s only by accepting the correctness of this statement that we can begin to glimpse how it might be wrong.<p>It is right that there is no one big answer <i>that will work for any program</i>.  There is no algorithm, no language, no logic, no formalism, no decision procedure that will solve the problem, and there never will be.<p>But I&#x27;ll wager that we can get much much better at &quot;apply[ing] lots of ad hoc techniques&quot; -- to the point that <i>in practice, for the programs we actually care about verifying</i>, it will <i>eventually</i> be possible to automate most of the verification process even for our largest programs.<p>If you look at what deep learning is -- to take one example of how this could happen -- it&#x27;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 <i>something</i>, but we don&#x27;t even need to know what.<p>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.<p>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 &quot;a significant fraction&quot;!  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&#x27;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, <i>and yet we can do it to a point</i>.<p>What we have that the machine doesn&#x27;t have is an amazing pattern-matching ability.  We&#x27;re seeing that machines are getting a lot better at pattern matching.  What the machine has that we don&#x27;t is massive reliable memory and absolute indefatigability.<p>Just to be clear, I&#x27;m not suggesting that pattern matching is all that stands between us and proving Goldbach&#x27;s conjecture.  (If that were true, we would have done it.)  I&#x27;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&#x27;t even very long.  (What makes them hard is, to return to the author&#x27;s theme, <i>complexity</i>.  To prove any particular fact about a large program requires figuring out what facts about the program are even relevant to one&#x27;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.)