3 ms·
I'd like to see more proof-carrying code techniques extended to WASM. Some of the work could be handed off to the compiler, embedding the proof in the binary. T
by smasher164 6y ago
I'd like to see more proof-carrying code techniques extended to WASM. Some of the work could be handed off to the compiler, embedding the proof in the binary. This could make expensive proofs, like termination checking, more tractable.
- rubatuga 6y agoare you aware of the halting problem?
- smasher164 6y agouh..yeah. The halting problem doesn’t mean you can’t do termination checking. It just means there’s no general algorithm for deciding if a machine halts. We only care about the specific subset of programs that the compiler is able to prove properties about. https://en.m.wikipedia.org/wiki/Termination_analysis https://en.m.wikipedia.org/wiki/Termination_analysis