I think the main issue is that eBPF cannot have loops. It restricts the programs you can write. Wasm does not have that property, so you cannot prove that it will complete.
To be clear, eBPF programs can have loops -- they're just jumps that have negative offsets (which are signed 16-bit numbers), but for security reasons many verifiers do not allow them so they can ensure that the program halts.
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.
uh..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.
