[kentonv]

> Strong type systems can give provably correct code.

In theory, perhaps. In practice, the compiler / runtime will have bugs. So you still need a sandboxing layer. Best to do both.

(The sandbox will have bugs too. But if you have two layers, hopefully it's hard for attackers to get ahold of zero days for both at the same time...)

[anyfoo]

Yeah, anything can be implemented incorrectly. My point was specifically that ignoring memory safe languages in favor of post-exploit mitigation is foolish, not that the latter is useless.

But in practice, type systems can be proven to be sound, implementations of type checkers can be proven correct, and while it’s still possible to make mistakes there, that isn’t so much an issue in mathematics, simply because of how rigorous it is. This does not just include type systems, there’s even an effort to rebase the foundation of mathematics on a type system instead of set theory!

In other words, we likely agree that steel vaults can have holes. But we probably also agree that an average steel vault is better in keeping things in or out of it than a velvet curtain.

[lmm]

> In theory, perhaps. In practice, the compiler / runtime will have bugs.

They probably won't. The trusted kernel for these systems is tiny; a sandbox is orders of magnitude more complex with orders of magnitude more chances for bugs to creep in.