On the Possibility of Certified Computation as a Physical Law: A Conceptual Framework
Every programming language built to date separates the program from the proof about the program. The program is written; the proof is established separately, through testing, verification, or formal methods. This paper proposes that this separation is not a necessary feature of computation but an architectural choice a...