[andor]

1) The halting problem only states that you cannot create a program that can decide whether any given program will finish. It is possible for special cases, though.

2) They didn't automatically verify the kernel. Coq is a proof assistant.

[DannyBee]

The halting problem is also decidable for finite memory machine, like our real ones, so ...

[cantankerous]

Yes, but our memory is so big and our machines can have so many states that the problem is still intractable in the general case.

[maaku]

But still very much solvable in the specific domains of real world applications.

[cantankerous]

You know what. I think I agree with you. I would actually go as far as to posit that most common applications don't require a Turing-Complete environment to run. If you could strip away the trouble spots and limit yourself to what you really need you can get a lot back in terms of software checking and assurance.

[shelf]

http://www.cs.dartmouth.edu/~sergey/langsec/occupy/

[cantankerous]

That's awesome. Thanks for sharing. It's nice to know that people a lot smarter than me are thinking about this already :).