Hacker News Reader

This is exactly how Windows' device drivers work. What you are asking for is the same functionality be extended to userland programs.

The primary problem for this is proof generation. Programming paradigms where proofs are easy to generate would be too limiting. So, although we gain security, our flexibility is tarnished.

View on HN

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.

Reply on news.ycombinator.com