4 ms·

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, tho

by andor 13y ago

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 13y ago
The halting problem is also decidable for finite memory machine, like our real ones, so ...
- cantankerous 13y ago
  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 13y ago
    But still very much solvable in the specific domains of real world applications.
    - cantankerous 13y ago
      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 13y ago
        http://www.cs.dartmouth.edu/~sergey/langsec/occupy/ http://www.cs.dartmouth.edu/~sergey/langsec/occupy/
        cantankerous 13y ago
        That's awesome. Thanks for sharing. It's nice to know that people a lot smarter than me are thinking about this already :).