Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

RustBelt: securing the foundations of the Rust programming language

dl.acm.org

Post reply on HN
Print view View original

31–40 of 109 posts

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

#31

Post by StavrosK »

nukeop wrote: 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 main difference that I've seen between C and Rust compiler errors is that, with C, my reaction is "goddamnit, you know what I mean, why can't you just accept it?!", whereas with Rust my reaction is "oh yes, I see how that may cause problems".

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

#32

Post by phkahler »

rntz wrote: post #29
dmix wrote: post #22

Earlier quoted context omitted.

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

We regard "this program is hard to test" as a problem that's worth refactoring to fix; why shouldn't we regard "this program is hard to verify" the same way?

But "this language is hard to verify" should not trump the usability of the language. The verification only needs to be done once, while the language will be used to write code again and again. If it doesn't negatively affect the language users then sure, change it to make verification easier.

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

#33

Post by pcwalton »

nukeop wrote: 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 secure than programs written in memory-safe languages. Obviously, that's not the case.

> seriously doubt that developers with real-world experience can like or even accept most of what this language represents.

Lots of developers with real-world experience, including me, use Rust all the time without any more problems than they would have in any other language.

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

#34

Post by currymj »

dmix wrote: post #22
chrismorgan wrote: post #3

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

people often mention forcing refactoring/rewrites as a benefit of unit testing, that you end up with code that is actually better in testing-unrelated ways. this is true in my experience.

i wonder how true this is of formal verification? especially in a language like Rust that has a fairly fancy type system?

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

#35

Post by pcwalton »

ZenoArrow wrote: post #23
mkesper wrote: post #10

Earlier quoted context omitted.

Rust is a direct contender to C and C++, not to script or GC languages. Please compare apples to apples.

For some languages, that distinction doesn't seem to apply. For example, it seems that the D language can be treated as both a scripting language and a system language, as the speed of compilation + execution can be comparable to that of scripting languages. For evidence of this, take a look at the first D versus Python comparison in this article, note that both scripts have comparable execution times (both finished…

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.

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

#36

Post by monocasa »

phkahler wrote: post #32
rntz wrote: post #29

Earlier quoted context omitted.

We regard "this program is hard to test" as a problem that's worth refactoring to fix; why shouldn't we regard "this program is hard to verify" the same way?

But "this language is hard to verify" should not trump the usability of the language. The verification only needs to be done once, while the language will be used to write code again and again. If it doesn't negatively affect the language users then sure, change it to make verification easier.

You need to reverify when you change the code too. Otherwise you could make the same arguments about testable code.

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

#37

Post by dtornabene »

Asdfbla wrote: post #5

I think I can understand and appreciate many different aspects of Computer science, but programming language theory truly is a bit too arcane and formal for me. I still try to follow it somewhat though (like when the Morning Paper had its nice writeup about RustBelt) and I enjoy learning Rust (which exposes you to the theory underlying its design more than other languages). Maybe it's good that the results of formal…

I felt a similar way for a long time. Software Foundations by Pierce (and a few other similar books) worked for me personally, by illuminating verification of PL through a programming-like environment. Scripting proof automation was enlightening is what I'm trying to say. If you haven't given it a shot and have the time, check it out.

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

#38

Post by Scaevolus »

crb002 wrote: post #28

Do this at the LLVM level and you get way more languages for free.

You've lost most of the semantics by the time you're at LLVM bitcode, since the high-level abstractions have been lowered into a basic for.

Rust's type system provides memory and race safety, but those details are lost at a lower level. It's very hard to analyze data races at the assembly level!

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

#39

Post by nine_k »

phkahler wrote: post #32
rntz wrote: post #29

Earlier quoted context omitted.

We regard "this program is hard to test" as a problem that's worth refactoring to fix; why shouldn't we regard "this program is hard to verify" the same way?

But "this language is hard to verify" should not trump the usability of the language. The verification only needs to be done once, while the language will be used to write code again and again. If it doesn't negatively affect the language users then sure, change it to make verification easier.

It depends on the cost of a defect. A language used for aircraft control software is going to have much stricter requirements for static analysis that a language used to create a website with cute pictures of kittens — even if happens to be the very same language.

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

#40

Post by ZenoArrow »

pcwalton wrote: post #35
ZenoArrow wrote: post #23

Earlier quoted context omitted.

For some languages, that distinction doesn't seem to apply. For example, it seems that the D language can be treated as both a scripting language and a system language, as the speed of compilation + execution can be comparable to that of scripting languages. For evidence of this, take a look at the first D versus Python comparison in this article, note that both scripts have comparable execution times (both finished…

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 as a criticism, I admire what the Rust team are doing, and will be glad to check out the language again in the future.

Post reply on HN