3 ms·
> The halting problem says that you cannot make this guarantee for ANY sufficiently complex program. That is correct but also completely irrelevant. In practic
by mbrodersen 4y ago
> The halting problem says that you cannot make this guarantee for ANY sufficiently complex program.
That is correct but also completely irrelevant. In practice all software we actually use and need can be written in languages that are slightly less powerfully than Turing complete languages. Look at CompCert, seL4, Dafny, Coq, LEAN, F-Star etc. etc.