10 ms·
Since tomp objects to trusting code, then I agree with Manishearth: if you're never willing to trust code, then you can never have guarantees. Even the proof
by scott_s 11y ago
Since tomp objects to trusting code, then I agree with
Manishearth: if you're never willing to trust code, then you can never have guarantees. Even the proof engine is trusted code.
- tomp 11y agoWell, you have to trust something... Silicone manufacturer, CPU designer, the OS, the compiler... But the big difference is, if I can do proofs and the compiler breaks my trust, that's a bug in the compiler. On the orher hand, Rust disallows complex proofs entirely, so I have to use unsafe code and trust random humans!
- Rusky 11y agoThe compiler is just as much written by random humans as anything else.