> That is, I don't think one can say that the reason why human-aided verification is unfeasible for some projects

That's not exactly what I said, or at least not what I think. I think that full, 100% confidence verification (the method is irrelevant) has some serious challenges as suggested by those theorems, and that it is, therefore, unjustified to believe that there would be a clear solution any time soon. One way to circumvent those challenges is, for example, to reduce the level of confidence.

> Yes, verifying the Linux kernel would take too much time, but not because of any specific theorem in theoretical computer science.

I'm not saying it definitely is, but I don't think anyone can say it isn't, either (well, technically, a theorem won't likely apply to a specific piece of code, except as a sample from some distribution).

> The reason why I am emphasizing this point is that I believe that referring to theoretical results in discussions like this makes it seems as though there is some kind of fundamental limitation that prevents people from verifying the Linux kernel in a proof assistant.

I think that the fundamental limitation (about the general case) suggests great challenges. And again, the specific method doesn't matter as long as it's sound. A proof assistant and a model checker are both bound by those results, as both are sound.

> Even though it is quite a jump to conclude that from theoretical results, especially when human intuition is involved.

I'm not sure human intuition is very relevant. We've had human intuition and proof assistants for the past 40 years, and still we haven't been able to prove software beyond a very small size. So I think that at the very least we should consider the possibility that if we can jump two feet up, then even though it seems like jumping all the way to the moon is a matter of degree, there just could be some fundamental obstacles in the way. I'm not saying we can't overcome them, but I'm saying we can't assume they're not there.

> But not because of a mathematical theorem. Some things are just a lot of work without there being a deep reason behind it.

OK, but people have written the Linux kernel, and that's a lot of work, too. Don't you think that if a mathematical theorem says that, in the worst case, A is much harder than B, and that in practice, A is, indeed, much harder than B, then maybe theory has something to do with it?

> We can go much further with deductive verification combined with automated verification compared to automated verification alone, precisely because human intuition can be used to guide the automated tools.

I think that's speculation and that it's unjustified by either theory or practice. It's unjustified by theory because if human intuition can consistently prove successful (to the point of being an industry technique), then whatever method is used suggests some recognized easier-than-worst-case subset, and so automated tools could take advantage of that, too.

It's unjustified by practice because you could have said the same thing thirty years ago, and here we are now, and automated tools are doing better on average (it's kind of complicated to compare, because there are cases where either one is much better than the other, but overall, when we look at "verification throughput", automated methods verify more software more cheaply). It is true that automated tools have some limitations that we haven't been able to break through, but so do manual proofs.