After a bit of searching, proof carrying code seems to be related to what I'm describing [3]. So I guess my point is: Does it really matter that you can come u

After a bit of searching, proof carrying code seems to be related to what I'm describing [3]. So I guess my point is: Does it really matter that you can come up with arbitrary programs that I will be unable to determine if they halt, if I can build up an entire OS platform of provably correct machine code with correctness proofs that I can scan out of a file to verify? Ultimately, here's the point of re-framing it like this in the first place: Now it's just a tooling problem. I recognize that this is a very big 'just'. [3] https://people.eecs.berkeley.edu/~necula/pcc.html https://people.eecs.berkeley.edu/~necula/pcc.html