10 ms·
The shallowness of rusts correctness has pretty much killed my interest in it. Much of its purported virtue seems to be mostly lore and myth, and doesn't keep
by j-pb 5y ago
The shallowness of rusts correctness has pretty much killed my interest in it.
Much of its purported virtue seems to be mostly lore and myth, and doesn't keep its promises under close inspection and scrutiny.
For example the "Rustonomicon" is only half finished and doesn't have that much real insight that couldn't be gained from a lot of basic-ish rust tutorials.
The memory model is not propery defined and only kinda sorta borrowed from C++ as the article mentions.
The borrow checker has only been formally specified and veryfied in a much simplified form and only very recently [2] ,with the actual model "just being what the borrow checker implementation does".
Having a fancy datalog based borrow checker is cool, but I'd much rather have a formal specifiation of the semantics.
Rust took the big bang approach of building everything at once, implementing stuff first without any formal semantics and just floating on an iceberg of implementation definedness, with endless discussions on how things COULD be formalized.
That's pretty much the antithesis to rusts safety philosophy; it's teaching water but drinking barrels of wine.
It wants your code to be well defined and follow its rules, but its rules are completely arbitrary, not properly defined nor written down.
I wish instead they had just started with a small borrow checked core language, and grown it from there, like described in Guy Steeles talk on "growing a language" [1].
I feel that Zig is doing a much better job in this regard, they have a tiny well thoughought language with a rigorous semantic description, and a good reference document.
I'm sure it would be much easier to add a borrow checker to the well-defined-ness and correctness of Zig, than to make Rust well defined and correct.
Super friendly community though.
Who knows, maybe someday the language that people think rust is, will crystalize from that community through their collective effort, like a self fulfilling prophecy.
1. https://m.youtube.com/watch?v=lw6TaiXzHAE https://m.youtube.com/watch?v=lw6TaiXzHAE
2. https://arxiv.org/pdf/1903.00982.pdf https://arxiv.org/pdf/1903.00982.pdf
- kristoff_it 5y ago> I feel that Zig is doing a much better job in this regard Let's wait until Zig gets a proper specification before trying to argue that we're doing a good job. Rust is much more mature and I'm sure people have found, fixed and standardized things that we probably have never even experienced once, ever. Right now the compiler doesn't even implement the full language.
- otabdeveloper4 5y agoRust is for people who failed to learn C++ and went (language) shopping instead. What else did you expect?
- j-pb 5y agoIf anything it's rust attempt to appease C++ programmers that caused this dilemma. Both have too much complexity for verified correctness.
- pcwalton 5y agoIn reality, the #1 thing that helps to verify correctness, if that if what you are after, is memory safety, something Rust has and Zig does not. In fact, in one common PL sense, a language that is not memory safe cannot be "verified correct", because what people usually mean by "verified correct" is type safety proofs, and obviously you can't prove a language type-safe if it isn't type-safe.
- j-pb 5y agoTo quote from Dijkstras essay "On the cruelty of really teaching computing science". > Right from the beginning, and all through the course, we stress that the programmer's task is not just to write down a program, but that his main task is to give a formal proof that the program he proposes meets the equally formal functional specification. While designing proofs and programs hand in hand, the student gets ample opportunity to perfect his manipulative agility with the predicate calculus. Finally, in order to drive home the message that this introductory programming course is primarily a course in formal mathematics, we see to it that the programming language in question has not been implemented on campus so that students are protected from the temptation to test their programs. And this concludes the sketch of my proposal for an introductory programming course for freshmen. There are more ways to proof correctness than through the type system alone. Would I prefer Zig to have a strong type system? Absolutely, but the reason why I choose Zig as a comparator is not because I feel that it does a significantly better Job at correctness than Rust, neither do fully. (And if I had to build something verifiably correct I'd probably Idris with linear types or something.) But I feel that with Zig I'd at least have the chance to proof the correctness of my program manually (with pen & paper). Although Zig is still heavily in flux it's simple and focused enough that it "being done", and me thus being able to understand it in its entirety, is at least visible on the horizon. With Rusts complexity that date is much further out into the future, if it is ever achievable. And even then, I'm not sure that I could fit enough of the Rust language and std into my head to be satisfied with the correctness of my proofs. Nor am I convinced that it can fit into the compiler devs heads sufficiently to ensure that the compiler is behaving correctly.
- orf 5y ago“Well thought out languages with rigorous semantic descriptions” never win because those are mostly meaningless metrics. The ability to get things done and the barrier to entry are the only metrics that count. See: JavaScript. While Rust is well thought out it’s killer feature is it’s the somewhat unique ability to allow people to get things done relatively quickly (sometimes/often with the expressiveness you’d expect from Ruby or Python) whilst also offering gigantic correctness guarantees and a (initially) low barrier to entry. But hey, Zig has a reference document. Watch out World!
- lmm 5y ago> “Well thought out languages with rigorous semantic descriptions” never win because those are mostly meaningless metrics. The ability to get things done and the barrier to entry are the only metrics that count. Perl was successful for a time but its messiness eventually caught up to it. OCaml is of the same vintage and grew much more slowly but I dare say it has a brighter future.
- IshKebab 5y agoI don't think Rust is messy in the same way Perl is simply because nobody has written a formal specification.
- nyanpasu64 5y agoUnsafe Rust, the undecided interactions between &mut and raw pointers and Pin (whether &mut should invalidate raw pointers permanently or until the &mut ends, whether Pin<&mut T> should be noalias), whether Vec is marked noalias (it isn't) or Box should be (it is), is a mess of undecided semantics that people are nonetheless writing code that hopefully won't be declared illegal in a future compiler version.
- zozbot234 5y agoThe scope of noalias semantics can be formalized quite precisely by using separation logic, which can also act as a simpler and more elegant foundation for Rust's reference semantics and the so-called borrow-checker. Future editions of Rust will probably do this at some point in order to gain these benefits.
- steveklabnik 5y agoThe borrow checker wasn't conceived of until Rust had been in the works for years, so that's one reason why that wasn't what happened. The language was grown. It just wasn't grown with an initial central feature, it was grown with an initial problem that it was trying to solve: a concurrent, safe systems language. As Rust explored the problem space, tradeoffs were identified, some were weighed differently than previously, some new strategies for solving these problems were discovered, and things were refined. Verification is actively underway. It's totally understandable to want to wait until it's here, but that doesn't mean it's impossible, just nontrivial. (Also, there are more papers that are older, like https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf from 2018, which this paper cites.)
- j-pb 5y agoThanks for the Paper! I'm looking forward to spend my weekend with it. Normally I'm a huge fan of a philosophy of backwards compatibility. Clojure has shown that it is possible with enough dedication. But I feel like it's a liability with the lineage you describe for Rust, the problem space was just too unexplored and vast, and the language has grown too large. Joe Armstrong has a joke in one of his keynotes [1], that after you've written the first version of something you should throw it away completely, because you didn't understand the problem at all when you wrote your solution, and now you understand it a bit better. A bit like how the web would be a much less ghastly ecosystem if we hadn't abandoned versioning for living documents which force every behaviour ever to interact, and god forbid be compatible, with one another, in a combinatorial hairball. Modern browsers would be less unwieldy if they just shipped 30 different rendering engines, one for each major revision, than ship a blob that purportedly is able to still render everyones Dogs website from the 90s (which is not true of course, it's just that nobody from the 90s is here to complain). It's a bit ironic that Rust fell into the same trap that caused the complexity that inspired its inception in the first place. Maybe once the major "features" for safe system programming were identified a new language (revision) should have started with only those features at its core. I fear that if such a language were to crop up now, Rust would just eat its children. [1]: https://www.youtube.com/watch?v=lKXe3HUG2l4 https://www.youtube.com/watch?v=lKXe3HUG2l4
- pcwalton 5y ago> I feel that Zig is doing a much better job in this regard, they have a tiny well thoughought language with a rigorous semantic description, and a good reference document. Zig doesn't have a "rigorous semantic description" that I can find. The reference manual is nowhere close. A "rigorous semantic description" would either be something like that of Java or, ideally, the operational semantics of Standard ML. I glanced through the "undefined behavior" section in the Zig reference and didn't see use-after-free anywhere. If it's that easy to find missing pieces then it isn't even close to complete. Wait until you start trying to define things like pointer provenance; it's not even clear what semantics LLVM is upholding. > Having a fancy datalog based borrow checker is cool, but I'd much rather have a formal specifiation of the semantics. There's a formal specification of the semantics of a subset of Rust via the RustBelt project. These things almost always start with a subset of the language; very few languages have full formal specifications, including type safety proofs and so forth. I should note that I'm not aware of any such work being done for Zig. > The memory model is not propery defined and only kinda sorta borrowed from C++ as the article mentions. Where's Zig's memory model? I didn't find it. I did find a GitHub issue [1], which has had far less discussion than that surrounding Rust's memory model. > I'm sure it would be much easier to add a borrow checker to the well-defined-ness and correctness of Zig, than to make Rust well defined and correct. No. This is just like the "just add a borrow checker to C++" meme that we used to see until it was shown to be infeasible. The problem is simple: if you can have mutable aliasing today in Zig, which you can, then the ecosystem has surely come to depend on it. So by forbidding mutable aliasing, you will break tons of code. It is not a reasonable subset of code to break; in C++ the set of code you break is "all methods" (because "this" has unrestricted aliasing), and I expect Zig to be no different. The borrow checker is not some magic dust that you sprinkle on a language to make it memory safe; the entire language, including all libraries, must be designed around it. Are you really going to break the doubly linked lists everyone has written? It is impossible to overstate how much memory safety in Rust is balanced on a delicate precipice; if the language has already fallen off the precipice I'm confident in saying it will never go back. (Well, unless you add a GC, which is what I'd do if I were in charge of Zig. There's nothing wrong with GC; it's the tool people have created for the very purpose of ensuring memory safety with unrestricted aliasing.) [1]: https://github.com/ziglang/zig/issues/6396 https://github.com/ziglang/zig/issues/6396
- lpapez 5y agoC++ has a standard that is thousands of pages long and I needed to look something up in it exactly zero times. On the other hand, I encountered hundreds of segfaults and race conditions and unlike Rust the well defined C++ language did nothing to prevent it. I would take a poorly specified borrow checker over extremely pedantic spec in a heartbeat.
- mike_hock 5y agoI drink milk daily and I've had to milk a cow exactly zero times. On the other hand, I've had to go to the grocery store to buy milk hundreds of times. Obviously the spec isn't meant to be a necessary read for end users.
- jepler 5y agoMy experience is different. The C/C++ (draft) standards documents are regular reference material for me, alongside web searches, man pages, & experimentation. (the draft standards are available for free in pdf format and for all practical purposes I've been able to treat them as the real thing) Experimentation is great for determining what the implementation you have right in front of you does, but not what is actually guaranteed. Trusted reference web pages are great (in fact, cppreference is AWESOME particularly for highlighting text that applies version-by-version of the C++ standard) but don't always cover everything. "I googled my error message" hits are so-so (but they may help you solve your problem) But the standard is the document that really lets you get into "how SHOULD it work", even while doing battle with 2 or 3 different compilers each of which implement a subset of the language you are theoretically programming in. (It's getting better, but finding a compatible subset of C++ supported by MSVC, gcc and clang used to be an interesting puzzle. And what a bummer to "switch to C++14" -- only with a list of caveats longer than most people will even read through, because of differential language & library support) I'd also just recommend becoming comfortable finding & extracting data from a daunting document like the C++ standard! It's a skill that will stand you in good stead, and I feel like being able to do this is one of the things that led to having my technical expertise well appreciated at work.
- littlestymaar 5y agoIt's a bit unsatisfactory, but it's juste how software works: with limited time, between a complete specification and no implementation, and an implementation without specification, the former will almost always win, because you get feedback and start building traction way earlier. Obviously it feels a bit of a mess, but messy fast-moving bazaars almost always win against cathedrals. Also, completely unrelated, I think it's really sad for Zig that it has become (against its creator will) the champion of the rust-hating crowd. Zig is cool and Andy's work on cross-compilation is a piece of art, but why is Zig in this discussion? Zig is definitely a “growing” language, not a language built on top of a formal spec. Zig doesn't have a defined memory model either!
- j-pb 5y agoI'm not arguing that Rust should be a Common Lisp like, Waterfall style cathedral. But for something a little less unwieldy that _could_ be specified without the collaborative effort of a hundred people. (Even more relevant now that Mozilla is no longer paying for those people.) Rust has a lot of great ideas, but it feels more like a prototype that got out of hand, than a focused safety oriented tool. Combine that with a healthy dose of over-optimistic marketing and wishful thinking and you got yourself a bubble. Rust is way too much cathedral than bazaar. Does it really have the need for a Macro system yet? Except for C++ template envy, JS has shown that transpilers are a workable alternative. Is the complex module system with access control necessary yet? Does the Std library need to be this comprehensive? > but why is Zig in this discussion? Simply because it's simple, and is perceived to target the same niche as Rust. I would have used Carp as a stand-in, but that's even more esoteric. I'd argue that neither Rust nor Zig actually target that niche properly, Rust is too complex to get the implementation and models right, while Zig is too conservative and not having the right model as a goal. Yet if I had to bet on either, it'd be on Zig simply because: There are two methods in software design. One is to make the program so simple, there are obviously no errors. The other is to make it so complicated, there are no obvious errors. -Tony Hoare
- littlestymaar 5y ago(TL;DR; Zig isn't simpler than Rust from an implementation perspective, quite the opposite. And the respective compiler size is a good illustration of that point) > Simply because it's simple But by what metric? For instance, why do you consider comptime being simpler than macros? Macros are a dedicated tool built for one specific job (compile-time pre-processing). Comptime means re-using the same syntax for both compile-time and run-time execution. Yes it is pretty elegant, and I like it but it is more complex that the Rust model because you now have a tool that needs to work with both cases. Same async, Rust has async functions and regular function, Zig has functions that are automagically coerced to the right type by the compiler. Is it ergonomic, probably (but not always), but it's much more complex to implement under the hood. Last but not least: memory safety, Zig's goal is to achieve a reasonable level of memory safety by using a collection of built-in sanitization tools. Those tools are much more complex than the borrow-checker (which rely on 2 simple rules: move semantic and shared XOR mutable)and for the most part they don't even exist! Zig's goal is developer ergonomics, and it's really cool to see radical experimentations in that space (and as I said, what zig has done with regard to cross-compilation is inspirational for every language author on this planet) but it's not simplicity. Otherwise, the Zig compiler probably wouldn't be 120% bigger than the rust one right?! (Rustc has 1.6 million loc[1], Zig has 3.5[2], more than twice as much. [1]: https://tokei.rs/b1/github/rust-lang/rust https://tokei.rs/b1/github/rust-lang/rust [2]: https://tokei.rs/b1/github/ziglang/zig https://tokei.rs/b1/github/ziglang/zig
- martin1975 5y agoUh oh, I sense a sequel Tannenbaum v Linus debate developing ...
- avgcorrection 5y agoMore like: pcwalton leaves a comment and the OP never replies to his comment