Remix.run Logo
▲ WorldMaker a day ago

The author of this article goes into the academic details on "Total languages" (under the headline "Limiting our scope") because they have been explored before. A specifically useful quote:

> The restriction made by total languages, therefore, does not help make verification any easier. Indeed, it would have been surprising to discover that an impossible problem becomes easy by restricting it just a bit (giving up leather seats does not reduce the cost of a car by 90%). We also note that every program could be trivially made total by adding a large counter, say 2^100 to all loops – this won’t change its physical semantics in any way – so we can already assume all real-world programs to be written in total languages without loss of generality. If total languages helped, we could have assumed all languages are total.

To rephrase it a little: all of our Turing Machines are limited (by RAM, by power, by transistor count, etc) compared to the Universal Turing Machine (infinite in scope, as a thought exercise), but that doesn't make solving safety or security easier.

If no one function can have 1000 calls, you make a million functions. If no one loop can go more than 1000 ticks, you put that in a function and call that function in a loop. Suddenly you have access to a million iterations through a loop.

The problem with Turing Machines is that even (intentionally) broken ones always tend to have unexpected sandbox escapes.