Post #4199195

@0xabad1dea@infosec.exchange an important thing to understand here is that software like theorem provers were designed around the assumption that the user cares about getting a correct answer This is also a property of compilers. No one (with the possible exception of CakeML) has successfully written a compiler that can treat the programmer as an adversary. This was one of the goals of Java: the compiler generates bytecode, which has some formally verified properties. This is then checked by a verifier and run through a JIT compiler. Java Applets were explicitly sold as using this to be able to sandbox Java: you can load Java and sandbox it and it's safe. Only it didn't work. JREs were so complicated that they had bugs. And these bugs led to sandbox escapes. The same thing happened with ActionScript (Flash) and JavaScript. Modern browsers no longer treat the JavaScript VM as a defensible boundary. They assume an attacker can escape from the JavaScript sandbox and get control over the renderer process, which they treat as the defensible boundary. The Rust core team is also explicit about this. Rust doesn't guarantee any of the nice type system properties against an a programmer who is actively trying to break them. The type system and borrow checker are tools for programmers to help them write code with entire bug categories eliminated (which is enormously valuable). They are not tools that are designed to guarantee that someone who can provide arbitrary text going into the compiler can't do malicious things (and there are over a hundred bugs in the rustc issue tracker marked 'soundness' that can lead to malicious code breaking some of the guarantees).