Live data from Hacker News

RustBelt: securing the foundations of the Rust programming language

dl.acm.org

41–50 of 109 posts

Re: RustBelt: securing the foundations of the Rust programming language

#41
post #8

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…

I don't see too many job offers for Rust developers, I see plenty for C and C++ though.

Re: RustBelt: securing the foundations of the Rust programming language

#42
post #2

Adrian 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…

FYI, (1) is (almost) definitely being addressed in the near future.

Re: RustBelt: securing the foundations of the Rust programming language

#43
post #22

My 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.…

That's sort of the trend of the industry for the past 50 some odd years, towards design for verification. First re-entrant code, then removing globals entirely, then splitting your dependencies out for testing, and recently there's been a bigger push towards formal verification.

Re: RustBelt: securing the foundations of the Rust programming language

#44
post #8

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…

I'm sorry you found Rust hard, but it really is a world apart from Perl. I started learning programming using assembly (Motorola 68k), and then went a different professional route (via Java and Javascript).

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

#45
post #20

Earlier 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…

Taking a trait object by reference is a pretty common pattern.

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

#46
post #22

My 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.…

> But he never mentions any other benefits or justification for changing how it works.

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

#47

Earlier 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…

You can, but there is a big difference: betterC is a subset of D, whereas unsafe Rust is a superset of safe Rust. That is, when you use unsafe, you don't lose any language features. When you drop into betterC, you do lose a bunch of stuff from D.

Re: RustBelt: securing the foundations of the Rust programming language

#48
post #21
post #8

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…

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.

Achieving Rust's safety in C took separation logic with the best tool probably being VCC from Microsoft. I encourage anyone that thinks the borrow checker is unnecessarily hard or alternative languages would be easy to try doing an existing Rust library or app in VCC with separation logic. Also, if applicable, ensure it passes soubd, static analysis to be free of any defects Rust's design would stop in that library that C doesnt.

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

#49
post #28

Do 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.

This raises an interesting question of whether Rust would make sense as a code generation target for other languages or runtimes. It is conceivable that you could compile and run untrusted Rust (with no unsafe blocks and restricted imports) the same way web browsers run untrusted JavaScript? It could be the only GC-less IR that you can run with a reasonable defense against memory corruption.

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

#50
> Rust is a new systems programming language that promises to overcome the seemingly fundamental tradeoff between high-level safety guarantees and low-level control over resource management. Unfortunately, none of Rust’s safety claims have been formally proven, and there is good reason to question whether they actually hold.

Aw, 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.

Post reply on HN