[helloTree]

How does this work, if the kernel is supposed to be TM-complete?

[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/

[riffraff]

I may be wrong, but AFAICT, the kernel in question is basically an API layer between the real browser and the OS.

The point of the exercise is to prove that something like a file read cannot be invoked with bad files and cannot cause buffer overflows etc..

That doesn't require turing completeness.