5 ms·
How does this work, if the kernel is supposed to be TM-complete?
by helloTree 13y ago
How does this work, if the kernel is supposed to be TM-complete?
- andor 13y ago1) 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 13y agoThe halting problem is also decidable for finite memory machine, like our real ones, so ...
- cantankerous 13y agoYes, 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 13y agoBut still very much solvable in the specific domains of real world applications.
- cantankerous 13y agoYou 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 13y agohttp://www.cs.dartmouth.edu/~sergey/langsec/occupy/ http://www.cs.dartmouth.edu/~sergey/langsec/occupy/
- cantankerous 13y agoThat's awesome. Thanks for sharing. It's nice to know that people a lot smarter than me are thinking about this already :).
- riffraff 13y agoI 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.