Hmm… „experienced“ can mean a lot of different things. I think in my original statement about Rust I was mostly thinking about programmers that aren’t ”experienced with Rust” being able to easily avoid memory unsafety. (Compared to programmers that aren’t “experienced with C++” being unable to easily avoid memory unsafety in C++.)
Well, what i am saying is that its not "easily" because the learning curve of rust is steep.
It does remind me of the learning curve I had with Ada -- you compile and you always work with the manual to understand the error. This is exactly the purpose of the very strongly typed language and compile time checks.
Just in Rust errors are sometimes (often?) not obvious to the novice and experienced developer alike -- and the tactics to overcome those errors are not obvious either -- unless you are experienced.
This shouldn't distract from Rust, given it great long term benefit and cost (and even liability) savings of having memory problems resolved during development.
1 Like
They are all wonderful features.
At the end of the day I'm here because of the promise of a safe language with the performance of C. I imagine many, who don't care about either, will not be swayed by all those other features, having invested a huge lot of time getting where they are with what they have.
3 Likes
I guess this all depends on what level of “easy” and what level of “experienced” we pick. In any case, IMO even the worst error message is infinitely easier to work with than hitting UB and getting a somewhat-working-somethat-broken program out of it without any indication of an error at all. Some of the things you’d do to run into tricky error messages in Rust, you probably would never (or at least should never) have dared to even try in C++.
Also most error messages in Rust are pretty good IMO.
Another point to keep in mind: Given the fact that probably most of us that can compare C++ to Rust can only judge them from a perspective of learning some C++ first and some Rust only later in life. It’s quite natural to feel that Rust is harder to program in when you go into learning it with the assumption that you can do everything that you could to in C++ (or at least in C) in pretty much the same way. Previous experience like that is probably also the main reason why people ever feel like the borrow checker is disallowing something for no apparent reason that ought to be okay. How else do you know that it really ought to be okay if it isn’t from previous experience with other languages like C/C++?
C and C++ do in fact have borrow checkers. They are called debuggers 
Or now a days, if one is lucky, the sanitzer tools can help out, msan, tsan, valgrind and the like. But they are not fool proof.
I'm more than happy that Rust complains about these things and forces me to think about it and get it right. I will gladly trade debugger time for compiler time.
2 Likes
Eek, but impressive. Turns out sed is Turing complete, too!
2 Likes
I've heard that many times, but am unconvinced. The learning curve for C++ is also incredibly steep, particularly as you are required to learn all the things that you can't do in order to gain the benefits of "modern C++". But I may be wrong, as it's been over a decade since I've relearned C++. Maybe they have a compiler flag now that makes old code fail to compile?
6 Likes
Ha! Well spotted.
If only.
1 Like
That is something that annoys me greatly...Lanaguages that change so significantly that they're practically a new language.
Javascript, C++, and to some degree C# all fall into this category.
I'd much rather learn an entirely new language than have to unlearn all the stuff I once knew which is now wrong (or at least deprecated, out of favor, etc.)
No matter how much Rust changes, I hope the language stays smallish and relatively simple (for some definition of simple).
2 Likes
My personal experience of the learning curve is somewhat different. I've programmed in 16 different languages, including some odd ones like Snobol 4 and APL. C++ isn't one of my languages, and it's not for lack of trying. I start by opening the C++ book, copying "Hello, world," and it runs. I then close the book, enter "Hello, world," and it fails. To make matters worse, I have no clue why. Ok. That's an exaggeration, but not much of one.
My experience with Rust is more line what I had learning other languages. With only a couple of exceptions, I was the only one in the building coding in the language, so I was pretty much on my own. It was also pre-Google and StackOverflow. I'd spend a week in total frustration, another week not making any real progress but feeling better, and another week finally getting something to run. I'd then start on a real project, but I typically didn't feel productive for another few weeks. That process was actually somewhat faster with Rust because of the excellent compiler error messages.
I think there may also be a bit of cognitive dissonance for C++ programmers coming to Rust. I see a lot of questions related to references being used the way you use pointers in those languages. I didn't have those problems, so maybe not learning C++ first shortened my learning curve.
5 Likes
It's great for experienced programmers, too. Over all these years of programming in C and C++, I never felt nearly as confident w.r.t the correctness of my programs as I did once I started programming in Rust.
YMMV. It wasn't for me after having learnt a good deal of modern C++, from where you can map the concepts almost one-to-one. Of course, if your primary language is Python or Java, then that doesn't help much.
I'm not sure if you are using "undecidable" in its technical sense here, or correctly at all. Rust has a very well-defined set of rules for what it considers memory safe, and it can always and definitely tell you whether your program qualifies as such. IOW, rustc will either compile your program or it will reject it, there's no middle ground where it throws up its hand and says "I don't know".
I might be more restrictive than it technically has to be, yes. But that "only" means it's trying to solve a hard problem.
Again, YMMV. I don't see many experienced Rust programmers asking about borrow checker errors here on URLO, for one. On the contrary, they tend to answer such questions with lightning speeds.
5 Likes
Isn't that the same conclusion that @m51 also draws in their post that you quoted?
Even though @grossdan might not have formulated it optimally, I think the general idea is correct, even in a technical sense. Rusts memory and ownership/borrowing model (as far as it even exists), or at least the stacked borrows model in particular, is inherently undecidabile, since it's kind-of “dynamic” in the sense that: UB is only triggered in code that actually gets executed. Statically determining that some code path is never taken is equivalent to solving the halting problem, i.e. undecidabile.
The borrow checker tries to statically prove that code doesn't contain any UB. It basically does this proof-finding with a heuristic and with the help of user-provided lifetime annotations and in a way that respects encapsulation (in order for crates not to break semver compatibility when function definitions are changed but their signatures aren't, and in order to make reasoning about code simpler). Interestingly, if unsafe code wasn't a thing, it wouldn't even really matter what exactly a lifetime annotation really means, as long as they help out the borrow checker and the borrow checker guarantees to not stop accepting code in the future that it currently accepts, and as long as some principles of encapsulation are upheld.
If the borrow checker is unable to prove your code sound then it rejects it, even though it might be totally fine in terms of stacked borrows semantics. The borrow checker can be improved/replaced with a more capable one, but it will always just stay an approximation of what code would theoretically be okay to be accepted. For example, such an improvement/replacement of the borrow checker was NLL and may come again with Polonius.
All of the above is just my personal understanding/opinion/interpretation, I haven't read the paper that @grossdan linked and I might be wrong with some of my observations.
Mhm, alright – so it seems to me that whether we consider borrowck "undecidable" depends on what we regard as fundamental:
- If we formulate borrowck in terms of all of correct computation, then we can say it's undecidable because there will be "obviously" (to a human) and dynamically correct programs that the compiler can't prove. In this case, the question being asked is: "Prove to me that this program does not dynamically exhibit UB".
- If we formulate borrowck in terms of the simple rules/heuristics it is actually implemented upon, then it can be called decidable: for each program, a set of simple predicates either holds xor does not hold. In this case, the question being asked is: "Evaluate the conjunction of these predicates P_i on the program text, and output a compile error if any of them is false", and this is purely a syntactic question.
The connection between the two formulations is then that the set of programs deemed compilable by #2 is a strict subset of those compilable by a (hypothetical and impossible) implementation of #1. They are not equivalent, because the questions being asked to the compiler are completely different. I guess this is the difference between the memory model of the abstract machine (#1) and the implementation of borrowck (#2).
Yet another way of seeing this could be necessary vs. sufficient conditions for correctness. A real borrowck impl can search for stronger, sufficient conditions, but not all of those conditions are necessary. These sufficient but not necessary conditions cause some programs to be rejected.
4 Likes
I inadvertently constructed a program that the compiler gave up on. It didn't report any errors, but the compiler didn't produce a result, either. The advice I got was to increase the recursion depth, which I did, and the program compiled correctly after a loooong time. From that experience I presume there are correct programs (in the compiler sense) with an effectively infinite recursion depth.
This is indeed another way in which Rust is undecidabile. However, AFAIK, the parts of the type system that are responsible for this don't have too much to do with the borrow checker.
Also this “recursion-depth” undecidability is a case where correct programs still are at least semidecidable (as in: at least all the correct programs will eventually finish compiling when you set an infinite recursion depth), while with the dynamic memory safety semantics undecidability that I explained above, all we can hope to achieve is to prove all incorrect programs wrong eventually (so might still be having co-semidecidability in this regard, I guess). Kind of like you can use miri to find undefined behavior in a program, but even after extensive testing you never know with 100% certainty if there isn't a code path leading to UB that you just never hit.
2 Likes
I think you indeed phrased it much better.
And, this is inherently the problem with Rust's compile time check -- and in particular an inexperienced Programmer might be mislead to think that the compiler is right -- and something is wrong with the programmers understanding -- all the while, the compiler actually used a broader heuristic than strictly necessary, to conclude an undecidable computation.
This is the key argument presented in the paper by Will Crichton I had referenced earlier -- which is based on his experience teaching Rust to students at Stanford.
Dan
1 Like
That seems rather an odd statement to me. Both Javascript and C++ are pretty much the most stable languages we have had over the decades. They both have rigorous and well maintained industrial standards, ISO and ECMA. They both have multiple implementations that are of high fidelity to their respective standard. They both go to to extreme lengths not to break old code bases when new standard versions are released. The result of all this is that JS and C++ from way back when still compiles and runs.
This is in stark contrast to, say, Python. Where a new revision breaks many things and as a result takes ten years to gain acceptance.
I don't think you gain anything by defining decidable as: any heuristic based algorithm that concludes its computation. Clearly, its designed to conclude, so you end up with a "tautology".
The notion of decidability exists in order to help classify problems, so that you can prove that a problem can not be solved in finite time by any kind of algorithm.
This is an important step, since it guides you to heuristics rather than try to think harder to find the perfect algorithm -- which will be futile.
In this sense, the memory check problem is undecidable, no matter what algorithm you come up with.
At most you can come up with a heuristic that is incomplete -- i.e. there will be perfectly correct Rust programs that the compiler will not identify, given its heuristics, and, apparently, given the heuristics, there are programs that the compiler flags as incorrect, but that are correct -- which requires tactics to overcome constraints put up by the heuristics -- and, in the worst case -- the creation of unsafe code to by-pass the compiler heuristics.
I think one example in the paper is how to deal with pointers into whole arrays and only single elements. The compiler "errs" on the safe side.
The guarantee you do get is that once its compiled, it will be correct, and for developers this is good enough -- but, novices and experts alike should be aware of this property of the compiler, and what these heuristics means for interpreting compiled results.
This is the key lesson I learned from the paper I cited earlier.
Dan
Rust provides fearless systems programming which C++ cannot provide. Quite the opposit, C++ requires the system programmers to be fearless.
6 Likes
There are. Type system constraints are Turing-complete on their own, and the constraint program must halt before compilation can continue. This happens entirely before the borrowck phase, but there may be other features that also lead to arbitrary computation within the compiler.
2 Likes