3 ms·

A verified compiler is not panacea, but rust is because of unsubstantiated claims of its marketing professionals? This is total nonsense.

• steveklabnik 5y ago
  Where did I say Rust is a panacea? A verified Rust compiler is a verified compiler, and wouldn’t be one either.
  • grumblenum 5y ago
    The stated goal of the grant program is to rewrite stable software many people use in Rust with the implied context being that C can’t be trusted, but Rust can be. I’m surprised that a language with no specified guarantees is favored over well established methods of verification. When you poopoo formal methods and verified compilers, it’s very hard to find a coherent logic behind RIIR, which offers much less in terms of security. Unless the exercise is a pretext to rationalize the grant money (which would be the real purpose).
    • howinteresting 5y ago
      The formal verification researchers I've worked with love Rust, because its type system nails the basics so they can focus on proving more interesting properties. Rust and formal verification work really well together. You can formally verify properties in a small section of critical code, then use the type and lifetime systems to expand those properties to the whole codebase. It's not an either/or, it's a both/and.
      • grumblenum 5y ago
        That's fascinating. Can you direct me to any of their papers or public work formally verifying a rust codebase? I haven't seen that before.