4 ms·

While I like what Rust is trying to achieve, I would never use something that is not formally proven. There are many, many other static analysis tools in the C

While I like what Rust is trying to achieve, I would never use something that is not formally proven. There are many, many other static analysis tools in the C and Ada world that can achieve exactly the same thing. They imply less risk, they are way more mature (~40 yo) and have bigger communities around them. Zig is a better C and C++. It should be used accordingly. It will do well in game servers, simulation servers and real-time systems that don't require hard safety constraints. Bonus points for Zig, it is a simple language and because of its nature it will be easy to build tooling around it to prove properties.

sam0x17 6y ago
Agreed that Rust has a bit of an odd fit -- it is in many ways a bit too onerous for day-to-day things like CRMs and web dev, but for the real scenarios where you want formal verification, you can of course also use actual formal methods and get a much higher degree of certainty perhaps. It is well suited for OS and driver dev though, which is arguably the target use case.
- jorangreef 6y ago
  "It is well suited for OS and driver dev though" Rust is brilliant, but for drivers, I would go for a language with OOM safety and strict static allocation, especially for embedded environments.
viraptor 6y ago
> that can achieve exactly the same thing That's a bold claim. What's the C formal validator which automatically handles both memory management and concurrency in source of any size within seconds/minutes? (Without making the source its own dialect rather than C)
- sam0x17 6y ago
  True, I'm familiar with ones in Java but not in C/C++. Having written a leak / double free detector for C, I have to say, you can only do so much statically and that wouldn't give me peace of mind exactly.
  - pjmlp 6y ago
    Frama-C and Microsoft's Security Description Language.
- johnnycerberus 6y ago
  I don't think we can call it "automatic handling", you just play by the borrow checker's rules. Automatic are the garbage collectors but not Rust's model. Anyway, you can verify the critical part of your C/Ada program by using: Why3 http://why3.lri.fr/ http://why3.lri.fr/ Frama-C http://frama-c.com/ http://frama-c.com/ (which is also extensible) SPARK https://www.adacore.com/about-spark https://www.adacore.com/about-spark One company that I've worked for used generators, they were specifying the model with a DSL and they generated the code based on that. Can't give more information about that but there are others doing the same (SpaceX and NASA). Rust is very good for people that don't have the resources and money to throw at or are working in an industry where they don't need a certification, for example I have friends at Amazon in Romania that build Firecracker, a virtual machine that is supposed to improve the safety story on AWS Lambda. And as an answer for your second question, at what cost? Also we don't know if Rust gets the scaling right. The compiler is already slow for the size of projects we already have.
  - viraptor 6y ago
    There's a bit of disjoint between what those tools do and they what Rust does. Rust provides something different - you write the source in standard code and get a sound app. Verifiers can't do that with C. You essentially either write a parallel list of annotations or generate the app from another language. It's a valid approach, but that's why I objected to "exactly the same thing".
smaddox 6y ago
Rust's borrow checking algorithm has been formally proven for a subset of the full language. Although this is one of those places where intuition is adequate to show the value, i.e. of enforcing exclusive mutability. After all, the intuition and implementation came before the proof (as is often the case).
sam_bristow 6y ago
There is work to get Rust qualified for safety critical domains [1]. Someone else pointed out that parts of the borrow checker have been formally proven already. Still a long road ahead, but I'm glad people are looking at it. https://ferrous-systems.com/blog/sealed-rust-the-pitch/ https://ferrous-systems.com/blog/sealed-rust-the-pitch/

sam0x17 6y ago

Agreed that Rust has a bit of an odd fit -- it is in many ways a bit too onerous for day-to-day things like CRMs and web dev, but for the real scenarios where you want formal verification, you can of course also use actual formal methods and get a much higher degree of certainty perhaps. It is well suited for OS and driver dev though, which is arguably the target use case.

jorangreef 6y ago
"It is well suited for OS and driver dev though" Rust is brilliant, but for drivers, I would go for a language with OOM safety and strict static allocation, especially for embedded environments.

viraptor 6y ago

> that can achieve exactly the same thing That's a bold claim. What's the C formal validator which automatically handles both memory management and concurrency in source of any size within seconds/minutes? (Without making the source its own dialect rather than C)

sam0x17 6y ago
True, I'm familiar with ones in Java but not in C/C++. Having written a leak / double free detector for C, I have to say, you can only do so much statically and that wouldn't give me peace of mind exactly.
- pjmlp 6y ago
  Frama-C and Microsoft's Security Description Language.
johnnycerberus 6y ago
I don't think we can call it "automatic handling", you just play by the borrow checker's rules. Automatic are the garbage collectors but not Rust's model. Anyway, you can verify the critical part of your C/Ada program by using: Why3 http://why3.lri.fr/ http://why3.lri.fr/ Frama-C http://frama-c.com/ http://frama-c.com/ (which is also extensible) SPARK https://www.adacore.com/about-spark https://www.adacore.com/about-spark One company that I've worked for used generators, they were specifying the model with a DSL and they generated the code based on that. Can't give more information about that but there are others doing the same (SpaceX and NASA). Rust is very good for people that don't have the resources and money to throw at or are working in an industry where they don't need a certification, for example I have friends at Amazon in Romania that build Firecracker, a virtual machine that is supposed to improve the safety story on AWS Lambda. And as an answer for your second question, at what cost? Also we don't know if Rust gets the scaling right. The compiler is already slow for the size of projects we already have.
- viraptor 6y ago
  There's a bit of disjoint between what those tools do and they what Rust does. Rust provides something different - you write the source in standard code and get a sound app. Verifiers can't do that with C. You essentially either write a parallel list of annotations or generate the app from another language. It's a valid approach, but that's why I objected to "exactly the same thing".

smaddox 6y ago

Rust's borrow checking algorithm has been formally proven for a subset of the full language. Although this is one of those places where intuition is adequate to show the value, i.e. of enforcing exclusive mutability. After all, the intuition and implementation came before the proof (as is often the case).

sam_bristow 6y ago

There is work to get Rust qualified for safety critical domains [1]. Someone else pointed out that parts of the borrow checker have been formally proven already. Still a long road ahead, but I'm glad people are looking at it. https://ferrous-systems.com/blog/sealed-rust-the-pitch/ https://ferrous-systems.com/blog/sealed-rust-the-pitch/