Comment by jeremyjh

11 days ago

There is a massive possibility space between “yolo” and formal proof. Rust has substantial evidence of correctness. For example, unit tests and types.

31 comments

jeremyjh

Reply
vrighter  11 days ago

That's verifying the implementation. The type system wasn't verified. It implements stuff perfectly, it has tests that prove it, but nobody formally verified that they perfectly implemented the correct algorithms

carlmr  11 days ago

[flagged]

  • _flux  11 days ago

    I think the difference is here:

    - If a compiled C++ program has unsound behavior, the program needs to be fixed

    - If a compiled safe Rust program has unsound behavior, the compiler needs to be fixed

    • bonzini  11 days ago

      > - If a compiled safe Rust program has unsound behavior, the compiler needs to be fixed

      Not really: the program still needs to be fixed, but fixing the compiler ensures that this unsound behavior never happens again to anyone. So you have two bugs to solve (vs C++'s one bug) but then you kill an entire class of unsoundness bugs just by recompiling.

    • jooops1  11 days ago

      That's not completely correct. If the Rust or C++ compiler has a bug in both cases either the compiler has to be fixed or the program can be adjusted to work around said compiler bug If possible. However, It's fair to argue that the Rust compiler makes more assertions and is more complex, which results in a larger error surface.

    • afavour  11 days ago

      Which is better, surely? One fix for every program written in Rust vs everyone having to fix it themselves…

    • devmor  11 days ago

      > If a compiled safe Rust program has unsound behavior, the compiler needs to be fixed

      Can you provide an example of such a program that can’t be fixed at the program level like a C++ example?

      13 replies →

  • krona  11 days ago

    > You can be annoyed by Rust fanboys, sure, but the more annoying are the Rust haters, because the hate always comes from a place of ignorance.

    For what it's worth, Rust fanboys also seem just as vulnerable to their ignorance of C/C++ compiler extensions and tooling (e.g. sanitizers, bounds annotations, standard library hardening modes and so on.) which are just normal part of professional C/C++ use today.