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