3 ms·
Yes please. And everything should be proved using the Coq programming language.
by speedgoose 5y ago
Yes please. And everything should be proved using the Coq programming language.
- AYoung010 5y agoI prefer my web browsers to be written exclusively in provably-safe ADA, for maximum security
- stingraycharles 5y agoOn that note, has the Rust compiler/runtime ever been formally verified?
- steveklabnik 5y agoA subset of the type system and standard library has been, but not the whole thing. It’s foundational stuff though so that was really great.