Hacker News Reader

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.

View on HN

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

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.

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

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.

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

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

Reply on news.ycombinator.com