I have recently performed a relatively simple development by using programming languages on which I had low-to-to-no experience: Perl (low), Ruby (no), Rust (no) and Go (no). Note that I am quite adaptable on the programming language front and that this small experiment was precisely meant to showcase these adaptability skills. Rust was, by far, the most difficult-to-learn, difficult-to-research, counter-intuitive, u…
> The most ironic part is that so many restrictions and problems are likely to provoke people to rely on whatever option happens to work, which might not be the best/safest one. Programs written in Rust are empirically safer than programs written in C or C++. > The higher the freedom, the better the results delivered by a sensible/knowledgeable person. If that were true, then C and C++ code would be safer and more se…
RustBelt: securing the foundations of the Rust programming language
41–50 of 109 posts
Re: RustBelt: securing the foundations of the Rust programming language
#42Adrian Colyer did a good write up of this paper recently on The Morning Paper : https://blog.acolyer.org/2018/01/18/rustbelt-securing-the-fo...
From the Adrian Colyer's review, we find the title might be misleading depending on what ownership model entails for a given developer’s use of the language: “We had to make some concessions in our modelling: we do not model… 1. more relaxed forms of atomic accesses, which Rust uses for efficiency in libraries like Arc 2. Rust’s trait objects, which can pose safety issues due to their interactions with lifetimes 3. s…
Re: RustBelt: securing the foundations of the Rust programming language
#43My favourite part: > our verification work resulted in uncovering and fixing a bug in Rust’s standard library, demonstrating that our model of Rust is realistic enough to be useful. The bug was https://github.com/rust-lang/rust/issues/41622 .
One thing about formal verification, and a lesser extent automated testing, is that you often end up spending the majority of the time adapting the program or language to work with verification rather than actually solving a real-world problem or fixing a real bug. His third comment fits this category well. The problem set he describes was that the code is designed in a way that's ill suited for formal verification.…
Re: RustBelt: securing the foundations of the Rust programming language
#44I have recently performed a relatively simple development by using programming languages on which I had low-to-to-no experience: Perl (low), Ruby (no), Rust (no) and Go (no). Note that I am quite adaptable on the programming language front and that this small experiment was precisely meant to showcase these adaptability skills. Rust was, by far, the most difficult-to-learn, difficult-to-research, counter-intuitive, u…
Rust to me is back to basics. There is a stack, and there is a heap. Many languages mask this from you, but notably C/C++ doesn't, and although it's a notch up in complexity from Perl, the control you get over these aspects lets you write code that is equivalent to C/C++ in performance. Something Perl/Go can do for you under some scenarios, but mostly not.
Granted, not everyone needs/wants to understand or work closer to the system.
Re: RustBelt: securing the foundations of the Rust programming language
#45Earlier quoted context omitted.
Nit: IIRC one can receive a trait object through a stack based reference. fn trait_obj(foo: &Trait)...
Sorry, you are right about that. You can have trait objects without an allocator. I'm not sure how common a pattern that is. Many people like to avoid trait objects and just parameterize the function on a type bounded by the trait in that case. And impl Trait is replacing some of the other cases in which you had to return an allocated trait object. Anyhow, you're right, I was wrong that people couldn't be using trait…
Box is so pervasive because it's currently the easiest way to get type erasure in return position.
Re: RustBelt: securing the foundations of the Rust programming language
#46My favourite part: > our verification work resulted in uncovering and fixing a bug in Rust’s standard library, demonstrating that our model of Rust is realistic enough to be useful. The bug was https://github.com/rust-lang/rust/issues/41622 .
One thing about formal verification, and a lesser extent automated testing, is that you often end up spending the majority of the time adapting the program or language to work with verification rather than actually solving a real-world problem or fixing a real bug. His third comment fits this category well. The problem set he describes was that the code is designed in a way that's ill suited for formal verification.…
I read "it lets me write a program that has a data race", accompanied by a program that has a data race, as saying that the bug is that a language feature meant to provide mutual exclusion does not provide mutual exclusion. In a language one of whose main selling points is "you always get mutual exclusion". How is this not a bug?
The benefit of changing this bug is that the guarantees Rusts makes to programmers are actually guaranteed.
Re: RustBelt: securing the foundations of the Rust programming language
#47Earlier quoted context omitted.
There are effectively two Ds: one that's garbage collected and one that's manually memory managed and unsafe. I don't think you can really consider them equivalent: there's always a large difference in development friction when you move from a managed environment to an unmanaged one.
> "There are effectively two Ds" Could you not also say there are effectively two Rusts? https://doc.rust-lang.org/book/second-edition/ch19-01-unsafe... "Rust has a second language hiding out inside of it, unsafe Rust, which does not enforce these memory safety guarantees. Unsafe Rust works just like regular Rust does, but it gives you extra superpowers not available in safe Rust code." By the way, I don't say this a…
Re: RustBelt: securing the foundations of the Rust programming language
#48I have recently performed a relatively simple development by using programming languages on which I had low-to-to-no experience: Perl (low), Ruby (no), Rust (no) and Go (no). Note that I am quite adaptable on the programming language front and that this small experiment was precisely meant to showcase these adaptability skills. Rust was, by far, the most difficult-to-learn, difficult-to-research, counter-intuitive, u…
You have successfuly uncovered that Rust is a fundamentally different programming language, instead of a variation of the same. I feel that having learned Rust, any new language similar to Rust would have way lower learning curve. It is quite similar to the jump required from imperative to a funtional language. We may be missing a good name for a paradigm the Rust falls into.
Then you'll appreciate the work languages like Cyclone and then Rust save you. There's other models published and in development that might make the next one a bit easier. Yet, separation logic is the proper comparison to borrow checker and most programmers didnt try to learn it.
Re: RustBelt: securing the foundations of the Rust programming language
#49Do this at the LLVM level and you get way more languages for free.
You can't prove safety properties of something that isn't safe. LLVM IR sure isn't.
Looks like people have had this idea before: https://internals.rust-lang.org/t/safe-rust-sandboxing-untru...
On the other hand, maybe this role is better served by WebAssembly.
Re: RustBelt: securing the foundations of the Rust programming language
#50Aw, c'mon!?
Rust is Sudoku for super-smarties.
- - - -
I'm going to "double-down" on that: Rust-lang is a toy, a beautiful bauble for minds addicted to a certain kind of complexity. Rust isn't about producing production code, Rust is about producing Rust. Scratching that itch.
My point is that I feel like the time and energy spent on Rust won't ever be justified in terms of productive bug-free software, when compared against some other simpler language (Hopgood's Noether comes to mind) or approach.