Again, "safe" versus "unsafe" bytecode. The "safe" code does all of the checking at runtime. Effectively: write code mainly in "safe" code, or code that compile

Again, "safe" versus "unsafe" bytecode. The "safe" code does all of the checking at runtime. Effectively: write code mainly in "safe" code, or code that compiles down to "safe" code, with your compiler doing as many optimizations from "safe" to "unsafe" code as it can. It's only when you're trying to optimize for speed / ensure correctness that it becomes necessary to write "unsafe" code. So if your compiler to bytecode has issues with generating proofs, "all" that happens is that the resulting code is slower.