>>14175162It's possible to prove these things on a subset of computers, like an implementation of a specific algorithm.
It might be possible to find a meaningfully large subset of turing complete machines that we can prove useful properties for. But, I haven't seen any work doing this.