Formal leaning HN people: Does Rust just have better sales & marketing than C++? Or is it really better for safety and correctness?
* Rust is NOT a programming language with deep, well-integrated support for proof systems or state exploration e.g. TLA+.
* Rust is no Frama-C where static analysis and function contract support is far more apparent and important
* Rust is not ADA
* The previous items also arise and are quite important as a direct result of generality: to the extent Rust imposes (albeit with benefit) language design to avoid certain kinds of functional issues, those features can later become limitations as a pushy, over opinionated language. Therefore to have flexibility in designing fast code that's yet correct code one usually has to have the low-level ability of C/C++ augmented with formal tools.
I'm not seeing Rust do that. Now, I've made a couple of jokes elsewhere in HN about Rust's propensity to show up uninvited to every vaguely language issue and press its case --- ex. I was vacuuming the floor yesterday when Rust somehow got through the front door and was explaining how a Rust vacuum is so much better, or how I'd never need to vacuum again if I used Rust. But I am only half joking.
For the last year I've spent much of my time in GO after getting sick-and-tired of C++ build/language complexity for the previous 10+ years. I am somewhat aligned to others who rightly ask if speed is all that matters? (Recall the Meyers joke about Pavlov training and C/C++ programmers when it comes to speed).
Correctness counts too and if the compiler spends a little bit more I time I'd be fine with that if for distributed/parallel programming I've got good guarantees.
For those who use TLA, SPIN, Frama-C and other formal tools what's your take on this? I think designers of those kinds of formal tools will be surprised to learn some of their correctness aims were solved by Rust.
Rust makes it easy to write code that's very expressive (dynamic memory allocation etc) and has strong safety properties. Certainly easier than having to verify with SPARK or Frama-C. Rust's type system, especially traits and affine types, lets you encode a lot of important properties (e.g. typestates).
I'm gonna look at rust; we're a huge c/c++ shop so there's room from improvement here. Now no program is a spec and implementation in one. Thus rust ought to be careful about keeping all it's hammers in language alone. If rust is smart and particularly wants to move to distributed computing or csps correctness will have to take on more complex meanings that bad index or divide by zero.
Ada doesn't do safe dynamic memory deallocation, right? You'd need Ada.Unchecked_Deallocation.
That's fine in cases where you can statically define everything up front (which you can for many of the use cases that people use Ada for), but for a general-purpose OS kernel, it seems like you wouldn't get the level of safety or correctness from Ada that you would from either Rust or C++.
(Disclosure - I'm one of the authors of the prototype mentioned in the thread. I'd happily use Ada or Frama-C if I thought it would solve the problems needed for getting safe code into the Linux kernel, but it doesn't seem like they actually do.)
I think this thread is too narrow on correctness. Plenty of memory issues in C/C++ can be solved by library code i.e. not char buf[...] but std::string. Not raw pointers but RC-pointers. The idea that language strictures alone solve a substantial part of code correctness I think is something that people with more experience in particularly CSP computing ala TLA/SPIN would seriously doubt. And even on the nit pickier things ... RUST is gonna help me write lock-free code with CAS, memory fences? Really?
* Rust is NOT a programming language with deep, well-integrated support for proof systems or state exploration e.g. TLA+.
* Rust is no Frama-C where static analysis and function contract support is far more apparent and important
* Rust is not ADA
* The previous items also arise and are quite important as a direct result of generality: to the extent Rust imposes (albeit with benefit) language design to avoid certain kinds of functional issues, those features can later become limitations as a pushy, over opinionated language. Therefore to have flexibility in designing fast code that's yet correct code one usually has to have the low-level ability of C/C++ augmented with formal tools.
I'm not seeing Rust do that. Now, I've made a couple of jokes elsewhere in HN about Rust's propensity to show up uninvited to every vaguely language issue and press its case --- ex. I was vacuuming the floor yesterday when Rust somehow got through the front door and was explaining how a Rust vacuum is so much better, or how I'd never need to vacuum again if I used Rust. But I am only half joking.
For the last year I've spent much of my time in GO after getting sick-and-tired of C++ build/language complexity for the previous 10+ years. I am somewhat aligned to others who rightly ask if speed is all that matters? (Recall the Meyers joke about Pavlov training and C/C++ programmers when it comes to speed).
Correctness counts too and if the compiler spends a little bit more I time I'd be fine with that if for distributed/parallel programming I've got good guarantees.
For those who use TLA, SPIN, Frama-C and other formal tools what's your take on this? I think designers of those kinds of formal tools will be surprised to learn some of their correctness aims were solved by Rust.