Remix.run Logo
▲ bluGill 2 days ago

But again, I don't need the full Turing complete machine. I can just say something like no function can have more than 1000 calls in a fun, and similar for loops - that's suddenly going to take away a lot of your Turing machine.

I'm not sure where the limits we need to place are, but that's the reasonable place to start.

▲WorldMaker a day ago | parent [-]

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.