The PAC learning framework takes as one of its starting assumptions that the learner cannot be instructed as to the form of the answer. I think that's a stronger restriction than we need for this purpose. It's okay if we have to provide the learner with new concepts, as long as it can remember them and apply them appropriately after that.

(I'm not actually sure that deep learning, at least as it exists today, is going to be particularly useful for this problem. I was just trying to come up with an example that people would be familiar with.)

In the conclusion of the talk I say that the only way forward towards anything resembling a sufficiently general approach to verification. Any form of statistical analysis (which is what many current learning algorithms are) is simply an algorithmic view of that very statement. One of the attendees even asked if machine learning could assist in that empirical study, to which the answer is, of course! But it is important to understand that this is what the learning algorithms would do: empirically study human-written programs. I don't think there's currently a whole lot of research in that direction, though.

Yes, I think we agree on a lot of this. Where we seem to disagree is on the prospects for a "silver bullet". As much respect as I have for Fred Brooks, I have always thought he was too quick to dismiss the potential of AI (though admittedly, when he first wrote that essay, AI was much better known for its failures than its successes). In particular, this dismissive, oddly moralistic quote from Turski, that you've requoted, I think is absolute horseshit. (For one thing, I'd wager that the biotech people will actually solve the hair loss problem within the next 10 years. I sure hope so :-)

But we agree that it's essential to understand what has been proven to be impossible. There will be no algorithm (in the sense of an effective procedure that works on any input) for computing correctness of programs. Indeed, all the familiar tools of computer science are inadequate: languages, logics, indeed formalisms of any kind. They may all have roles to play, but none of them can be the silver bullet in and of itself. It is exactly as you say, that the breakthrough, if there is to be one, must come through empirical analysis of actual programs.

But we now live in a world where, at long last, a machine has beaten the world champion Go player. Many experts thought that wouldn't happen for decades. If we can do that, I think that means we are finally starting to have solutions to problems of perception and pattern-matching that have been stymieing us this whole time. I am very excited.

I probably came out sounding a little too combative at the beginning. I think you've written an excellent summary here (modulo the Turski quote :-), and I think it's kicked off a very interesting conversation. (Even Animats, I think, doesn't disagree with us as much as he/she initially appears to.)

> In my job, I formally specify and verify large, complex distributed systems.

I am actually working on a project to put some code where my mouth is: to build a reasoning system that uses AI and ML and learns to reason about programs. It's a long-term thing and I'm probably a couple of years from having anything to demo, but I'd love to learn more from you about the problems you encounter. Are you by any chance in Silicon Valley? If so, let's get together. My email is in my profile.

> I have always thought he was too quick to dismiss the potential of AI

I have no idea what AI is (in a practical context), and I think no one else does, either. Do you mean the statistical algorithms that people call machine learning?

> But we now live in a world where, at long last, a machine has beaten the world champion Go player.

It is very important to understand how that was achieved and the difference between that and verification. It's unknown how good Google's Go program is compared to some arbitrary opponent, as the algorithm it employs is not the algorithm to "win" at Go (which is far too computationally expensive to be feasible). It is "merely" able to beat other human players, but that is mostly because humans can beat human players, and the program learned from humans. Humans, however, do not efficiently verify other humans' programs, and that makes the problem very different.

Don't get me wrong: I think that statistics are absolutely necessary, and that machine learning could certainly help. But "help" does not necessarily mean "solve". At the end of the day, even if we pretend machine learning does resemble intelligence (which it does not, as any expert would tell you; we're still in the vicinity of zero IQ), we must remember that intelligence -- unlike what some people like to believe -- is not a very good "general problem solving" algorithm; it is a reasonable general algorithm for problems that humans tend to confront in many situations. For example, humans are even worse than computers in finding solutions to NP complete problems, and are in general terrible at solving many problems. In general, humans are good at forming conceptually deep but undetailed theories. Is verifying programs one of those problems that intelligence can solve? It could be, but we have no good theory that can give us intuition into whether it is or it isn't. I do know that a model checker was far better than me when reasoning about programs.

But instead of hypothesizing, a good first step would be to gather statistics, and to use machine learning in analyzing those statistics. I think it's more likely that machine learning would uncover important patterns that we could then exploit in more robust algorithms.

Thanks for the invitation, but I am very far away from Silicon Valley.