4 ms·
[I'm moving my comment from the flagged tree over here because I feel that it captures the spirit of my lament of Rust, and your interpretation of it being a pu
by j-pb 5y ago
[I'm moving my comment from the flagged tree over here because I feel that it captures the spirit of my lament of Rust, and your interpretation of it being a pure endorsement of Zig, rather well.]
TL;DR: Yes! But Zig is a Stand-in for simpler languages, and while in its infancy, I can foresee it to be "done" and "fit into my head". Rust requires a suspension of disbelief that all this complexity can be tamed and "gotten right" with a leap of faith for the language, compiler and everybody in-between including myself, that I'm not confident enough in the "proofs" it provides.
To 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.
Clojure programs are surprisingly high quality despite being dynamically typed.
I feel almost sorry to not write a lengthy counter rebuttal, but sadly I agree with everything you said!
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.
If I had to build something (computer)-verifiably correct I'd probably Idris with linear types or something, but that's not a real contender, and neither is Carp or Linear Haskell.
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 (especially if one compares the number of people working on Zig with the number of People working on Rust, although Carp might be an even better contender in that metric). 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 language into my head to be satisfied with the correctness of my proofs, ignoring the fact that it also has to fit into the compiler devs heads sufficiently to ensure that the compiler is behaving correctly.
My critique is that little of this complexity actually comes from the parts that make the language unique, non of it is essential, it's all incidental complexity.
It's in the macro system, the standard library, the hand-wavy semantics of "box" and compiler intrinsics, of magic low level traits, an overzealous module system, way to much fondness of abstractions and their removal by compiler magic, and a general nonchalantness towards C++'s complexity.
- pcwalton 5y ago> TL;DR: Yes! But Zig is a Stand-in for simpler languages, and while in its infancy, I can foresee it to be "done" and "fit into my head". I don't understand how something that isn't type-safe (memory safety is a subset of type safety) can be more "correct" than a language that is type-safe. It is certainly hard to prove Rust type-safe. But that's infinitely easier than proving something type-safe that trivially isn't type-safe! > way to much fondness of abstractions and their removal by compiler magic Heavy reliance on abstractions is what makes lifetimes and the borrow check practical. For example, Arc, Mutex, Cell, and RefCell are all abstractions that serve as library-defined extensions of the core lifetime rules and are generally optimized away by the compiler. I'm extremely skeptical that lifetimes/borrow checking can be made usable without this sort of thing. If a goal of Zig is to minimize abstractions, then that's yet another reason why adding a borrow check to it after the fact will not work. When Zig is "done", it will have to either (a) become memory safe by addition of Rust's lifetimes/borrow check (which is probably impossible, but if it were done it would bring about a lot of the things you say you don't like about Rust); (b) become memory safe by addition of a GC (which is the best option, but I doubt it will do so); (c) not be memory safe (which is probably what will happen). There is no free lunch. And then, assuming it chooses option (c), you run into this problem: Try as hard as you want, you will never be able to prove a language type-safe that isn't type-safe, no matter how simple that language is.
- j-pb 5y agoI've written correctness proofs for C code, both as part of my university classes and after. Unless rust has some kind of de brujn criterion (and properly formalising and bootstrapping it from a minimal core would be a step into that direction) the proof it produces is only as good as the entirety of the codebase. Correctness proofs are an inherently human thing, it's all about convincing your opponent of the proofs validity. One could of course build a language on inuitionistic math a a la coq, but that's neither practical nor realistic, so human checked proofs will have to do, and simplicity helps a lot with those. Edit: It feels like we're talking about subtly different definitions of correctness. I mainly care about correctness of specific program instances, whereas you are more concerned about the correctness of every instance expressable by the language.