No, I don&#x27;t believe that the future is languages that are not Turing-complete, mostly because halting is not the property most people care about. I believe that <i>a large part of</i> the future will be languages that are not Turing-complete, for applications where that&#x27;s appropriate (e.g., C compilers) but not where it&#x27;s not (e.g., interpreters). I also don&#x27;t think that &quot;well, that&#x27;s how we&#x27;ve always done it&quot; is a particularly compelling argument given how young the field of programming languages is.<p>For instance, another wonderful example of requiring code to cooperate with the proof process is Google&#x27;s Native Client. NaCl doesn&#x27;t care about halting; what it cares about is that the code in question only accesses its own memory, or makes specific pre-defined calls into the supervising code. You can do this with hardware support (and they did, with segmentation, where available), but you can also do this with software support.<p>The NaCl technique is straightforward. You&#x27;re required to lay out your assembly so that every 32-byte alignment boundary separates instructions; you must insert NOPs as necessary. Any fixed read, write, or jump must be within an address within a mask (or to a predefined address in privileged code), and any computed read, write, or jump must be immediately preceded, within the same 32-byte block, by a mask operation on the relevant register. For data, the mask enforces that only data is accessed; for jumps, the mask enforces that the jump target is within the code area and also 32-byte aligned.<p>Now you&#x27;ve proven a fairly complicated property of the code, that control flow never escapes to privileged code except at well-defined entry points. Doing so on arbitrary x86 would be impossible (unless you resort to binary translation), but this is a very minor modification to arbitrary x86, and a regular C compiler can be easily modified to emit it. The resulting restricted variant of x86 remains Turing-complete.<p>And it is entirely reasonable for the NaCl verifier to say &quot;Uh, what are you doing, please try again&quot; if presented with code that is technically non-malicious but does not follow the rules. The NaCl verifier doesn&#x27;t claim to detect malicious code (that&#x27;s the antivirus problem, and unsolvable). It claims to take code that makes a specific promise about not being malicious, and verifies that property.