|
> Moving theorem proving upstream into compilers, sandboxes, and the browser seems like the future The way I saw this proposed, back in the 2000s: "proof-carrying code."[0] The idea is: the compiler compiles the program, and simultaneously generates a proof that the program doesn't violate X, Y, or Z safety rules. Later, the end-user downloads the program and the proof together, and the local execution environment (the browser, the OS itself, etc) verifies that proof. The idea being: constructing proofs is hard and sometimes involves manual steps. But verifying a proof is easy and automatic. So do the slow, manual thing once, and the fast thing each time the program is downloaded. [0]: https://en.wikipedia.org/wiki/Proof-carrying_code |