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

91–100 of 109 posts

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

#91

Post by tom_mellior »

dmix wrote: post #64
tom_mellior wrote: post #46

Earlier quoted context omitted.

> 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? T…

I was specifically referring to the 3rd comment on the Github issues page, not the first comment which mention a race condition which the eventual commit addressed > His third comment fits this category well. And even then I was only talking about the language he used, aka the justifications and rationale he proposed, which seemed entirely around being difficult to verify formally, rather than mentioning any real hyp…

Fair enough about the particular Github comment, but even there I think you are wrong.

The architectural downside is being unable to understand a program you have written: "However, if the type does not have an explicit impl for Send/Sync, I don't know how to even figure this out -- I would have to chase all types (including safe ones, and across all abstractions) of all fields recursively and then check when they are Send/Sync... that's way too error-prone."

This doesn't just talk about his particular proof tool being unable to understand this. It's about any Rust developer being unable to easily understand the types used by their programs, using only standard library constructs. (If anything, this should be easier for tools than for humans.)

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

#92

Post by metargz »

namelost wrote: post #72
dbaupp wrote: post #65

Earlier quoted context omitted.

In this case, safer == memory safety (which is not a Rust-specific thing), not general forms of correctness, and the comparison in the original comment is to C and C++, not statically typed languages with a GC.

Unless it has been edited, the original comment doesn't say memory safety, it says "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" . The reply to that comment then interprets safety as memory safety and compares to C and C++. This is kind of my point. Rust defines safety as memory safety, but unfortunately memory safet…

> Whereas languages that achieve memory safety via a GC, allow me to focus my mental energy on writing correct code, not on memory management.

Ownership type systems are supposed to rule out synchronization errors (say, data races), which is something you may want regardless of how memory is managed. Say, the research on ownership types that came out of MIT in early '00s worked with a subset of Java (see OOPSLA'02 "Ownership Types for Safe Programming: Preventing Data Races and Deadlocks").

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

#93

Post by Blaisorblade0 »

sifoo wrote: post #74
ktpsns wrote: post #73

Earlier quoted context omitted.

From my knowledge, the ERC funds fundamental science. In my personal area (theoretical physics), people tend to move from Fortran to C++ nowadays. As an effect, mostly readability decreases (without linear algebra libraries) or the compiler doesn't help anymore with compile-time bound checks (so people use run-time bound checks with assertions instead). Not even to mention the years of wasted time for people finding…

How is questioning the choice of project to fund feeding trolls? I was under the impression that diversity was mostly considered a good thing, that has to go for perspectives as well. I just don't get why Rust desperately needs a lot more money than any other tool that's equally useful, they were already pretty well funded by other organizations.

This is one research grant on Rust among tons of grants on other projects. And it funds research. When somebody has equally valid research project on C, rest assured it’ll be funded as well, as it has already happened (EDIT) with research on abstract interpretation, separation logic and so on.

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

#94

Post by Blaisorblade0 »

p0nce wrote: post #76

Every post in this thread slightly criticizing Rust is greyed. This is an unfortunate part of being an overhyped language: no one is allowed to emit discordant opinions.

Rust can be criticized (https://news.ycombinator.com/item?id=16305437), but flaws will be spotted. I’ll concede nonsense on other topics might have more leeway.

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

#95

Post by Blaisorblade0 »

pcwalton wrote: post #30
crb002 wrote: 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.

Verification of unsafe languages such as unsafe Rust (here), or C, PHP or assembly (in other research) tries to show if some particular program is correct or not — by exhibiting bugs, proving safety, or both. Tons of approaches exist.

But verification can be easier for higher-level languages.

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

#96

Post by gliptic »

vectorEQ wrote: post #90

adding security features to a language itself seems a bit silly. it just adds complexity and bloat to the code (which has been and still is mostly unverified..) which gives people a sense of security that's most likely false (as people imagine hyped things to be bigger than they actually are). I'd say a good coder could write more seucre and sound code in C, though someone who isn't conscious of the nature of the lan…

There's nothing false about the sense of security. In fact, after I started using Rust, my C/C++ has become more disciplined as well. The idea that memory safety is "training wheels" is silly.

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

#97

Post by Const-me »

namelost wrote: post #61
pcwalton wrote: post #33

Earlier quoted context omitted.

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

> > 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++. But Rust defines safety as being safe from the kinds of errors that the Rust compiler is capable of making one safe from (buffer overflows, race conditions,…

> Rust is great for writing high-performance code

Some high-performance code is CPU bound. To approach advertised FLOPS figure on any modern CPU, you must manually write SIMD code (typically SSE, AVX, and/or NEON). It’s only in Rust nightly, and is very limited. Without SIMD, you’ll only use a small fraction of CPU’s computational power.

The only programming languages great for high-performance code are C and Fortran. C++ is also OK because C compatibility.

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

#98

Post by zerb »

currymj wrote: post #34
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.…

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?

Yeah, I'd say there's a huge overlap in attributes of testable code and reasonable code.

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

#99

Post by kahnpro »

vectorEQ wrote: post #90

adding security features to a language itself seems a bit silly. it just adds complexity and bloat to the code (which has been and still is mostly unverified..) which gives people a sense of security that's most likely false (as people imagine hyped things to be bigger than they actually are). I'd say a good coder could write more seucre and sound code in C, though someone who isn't conscious of the nature of the lan…

This is a very dangerous mindset.

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

#100

Post by steveklabnik »

Jweb_Guru wrote: post #86
namelost wrote: post #61

Earlier quoted context omitted.

> > 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++. But Rust defines safety as being safe from the kinds of errors that the Rust compiler is capable of making one safe from (buffer overflows, race conditions,…

> Rust is great for writing high-performance code, or code that needs to be parallelised within a single process. However if performance is not a concern then a statically typed language with a GC is usually a better choice. Are there Rust programmers who disagree with that?

It depends on context.

I don't think many would disagree that it would be easier, but better is very broad. Better in what way? For what purpose?

For example, if you already know Rust, then "easier" may (or may not, depending on what sense of easy you mean!) not be a compelling argument.

Rust is certainly not the best tool for every single task, but it also has broader applicability than "I can't possibly accept a GC."

Post reply on HN