10 ms·

RustBelt: securing the foundations of the Rust programming language

294 points by based2 9y ago

fovc 9y ago
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-foundations-of-the-rust-programming-language/ https://blog.acolyer.org/2018/01/18/rustbelt-securing-the-fo...
- nickpsecurity 9y ago
  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. stack unwinding when a panic occurs, which can cause similar issues to exception safety in C++ 4. automatic destruction, “which has already caused problems for which the Rust community still does not have a modular solution.” 5. a few details unrelated to ownership, such as type-polymorphic functions and “unsized” types.” Also shows why it’s good to have a semantics in the beginning covering the whole language like with ML or later SPARK Ada. It forces language developers to spot and address these corner cases early on. Good news is that, like with SPARK, one might just subset their use of Rust to exclusively what has been proven with no use of anything else. Is anything on the list common enough in most Rust development where it can’t be avoided and must be verified later? I’ve obviously seen many people mention traits. Arc and automatic destruction safety not being proven is a bit ironic given they’re presumably there to boost safety versus raw pointers and manual destruction. EDIT: Thanks for quick, clarifying replies about these. It's looking like a subsetting approach can work.
  - dikaiosune 9y ago
    For clarification, "trait objects" are a subset of the trait system, and have much less use in rust programs than traits overall. A trait object is a dynamically dispatched pointer (often owned through Box or Arc), as opposed to the usually statically dispatched generic usage of traits that's more common in rust. Destructors aren't guaranteed to run in Rust, they aren't necessary for memory safety. It's a fair concern to note that they aren't modeled, because they are pervasive and can impact memory safety, but they don't exist to support it. Panics not being modeled is of course also a big gap, although you could always compile your code with panic=abort if you wanted to dodge that issue!
  - lambda 9y ago
    You can avoid 1 if you do no multithreading, or if you accept a slower implementation of Arc. Embedded code in Rust almost always avoids 1, 2, 3, and 4. Arc is used for freeing dynamically allocated memory when all references, including across threads, are dropped, but if you're running without dynamic memory allocation, you don't need that. Trait objects also require allocation. Embedded targets also generally don't implement stack unwinding, and stack unwinding can be disabled on other targets as well; it's really only most useful in larger applications in which you want some threads to be able to continue running even if another thread panics. Automatic destruction can be fairly easily avoided if you're running without an allocator, as it is mostly used for freeing such allocated memory, as well as a few things like file handles and the like. The things covered in 5 might be harder to avoid, but also more likely to be amenable to being covered by further versions of the RustBelt work. So yes, using a subset of Rust without these features is quite feasible, and often done when working in embedded (aka no_std) code. I don't know SPARK Ada that well, but I believe it has similar constraints of no dynamic allocation. If you can do without dynamic allocation in Rust, many of the problematic features wouldn't be used.
    - dikaiosune 9y ago
      Nit: IIRC one can receive a trait object through a stack based reference. fn trait_obj(foo: &Trait)...
      - lambda 9y ago
        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 objects in an embedded context with no allocator, but I also think it's perfectly reasonable to write in a subset of Rust in which you don't use trait objects at all.
        Argorak 9y ago
  - Jweb_Guru 9y ago
    FYI, (1) is (almost) definitely being addressed in the near future.
- matt_d 9y ago
  Two recent talks about the project: - Derek Dreyer, Workshop on Software Correctness and Reliability 2017 (48 min): https://www.youtube.com/watch?v=Y9vemQmVeLI https://www.youtube.com/watch?v=Y9vemQmVeLI - Ralf Jung, POPL 2018 (25 min): https://plv.mpi-sws.org/rustbelt/popl18/ https://plv.mpi-sws.org/rustbelt/popl18/
  - fmap 9y ago
    Derek also gave a terrific keynote talk at POPL 2018 about the big picture: https://www.youtube.com/watch?v=8Xyk_dGcAwk https://www.youtube.com/watch?v=8Xyk_dGcAwk
chrismorgan 9y ago
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 https://github.com/rust-lang/rust/issues/41622.
- dmix 9y ago
  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. So I'm not sure it's necessarily a 'bug' in a traditional sense that supports the use of formal verification, except in some self-serving way. That said, I'm very much in support of formal verification in these types of languages.
  - rntz 9y ago
    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?
    - phkahler 9y ago
      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.
      - monocasa 9y ago
        You need to reverify when you change the code too. Otherwise you could make the same arguments about testable code.
bennofs 9y ago
Does this prove that the current borrowck rules are sufficient to catch all possible mistakes? For example, does it catch stuff like https://github.com/rust-lang/rust/issues/31287 https://github.com/rust-lang/rust/issues/31287 or https://github.com/rust-lang/rust/issues/38899 https://github.com/rust-lang/rust/issues/38899?
- lambda 9y ago
  What the paper demonstrates is that if you have a correct borrow checker, and you have the ability to create types using `unsafe` which can extend the semantics of the language to cover things that the borrow checker cannot cover, you can write proofs that demonstrate that the language is still sound given the addition of those types. This helps demonstrate that one of the fundamental design goals of Rust, have a simple but limited system of borrowing built into the language, and allow more complex forms of managing reference types safely built on top of it as library features using `unsafe`, is a fundamentally sound design. In other words, you don't have to treat the language and all libraries using `unsafe` as one large system that you need to prove soundness of, but you can do modular proofs of the core language, and each library that adds a new type of memory and reference management, independently. Those bugs you reference are simply bugs in Rust's borrow checker. The language used for the RustBelt paper, LambdaRust, is a language that is much simpler than Rust itself, making the borrow checking much easier but the language not as convenient to use (it is not intended to be used at all, just to act as a model of Rust). The things you reference are simply bugs, but because of the fairly expressive syntax that Rust offers actually getting the borrow checker right can be be difficult in some cases. I don't think that there are any theoretical concerns about the ability to write a correct borrow checker, just practical issues with the current implementation not correctly handling certain cases.
  - bennofs 9y ago
    > I don't think that there are any theoretical concerns about the ability to write a correct borrow checker, just practical issues with the current implementation not correctly handling certain cases. Is it really that trivial? When looking through https://github.com/rust-lang/rust/blob/master/src/librustc_borrowck/borrowck/README.md https://github.com/rust-lang/rust/blob/master/src/librustc_b..., it is not at all clear that these rules cover everything to me. There are some complex side conditions, isn't it easy to miss something there?
Asdfbla 9y ago
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 methods now find more practical application, so it's easier to get people (who aren't hardcore logicians) interested in the whole topic.
- dtornabene 9y ago
  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.
- pornel 9y ago
  I find Rust's RFC/design discussions fascinating. They're a mix of serious Programming Language Theory and practice. The same feature in Rust is seen by some as "algebraic data types" and "oh cool, I can add data to enums" by others. Some feature proposals starting with "wouldn't it be nice to have…" end up designed with input from people who literally have a PhD in this feature (and are bikesheded until people without PhDs can use the feature).
nukeop 9y ago
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, unfriendly, constrained, unappealing, etc. of all of them. Warnings and errors appeared systematically and, despite their verbosity, were rarely helpful. 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. Being so concerned about making sure that the generated code is extremely safe no matter what by sacrificing flexibility and user friendliness is far from ideal. Restrictions and prohibitions have always to be seen as an in-the-worst-case-scenario resource, not as a primary solution; much less when dealing with something as complex as programming, a very powerful tool supposed to be managed by knowledgeable individuals. The higher the freedom, the better the results delivered by a sensible/knowledgeable person. Unless Rust changes a lot, I don't see it going anywhere. It might get some support from theoretical/academical/inside-whatever-bubble circles, but seriously doubt that developers with real-world experience can like or even accept most of what this language represents.
- mkesper 9y ago
  Rust is a direct contender to C and C++, not to script or GC languages. Please compare apples to apples.
  - zzzcpan 9y ago
    Only for some code it's not apples to apples. For most code GC is not a big deal and the languages just offer different tradeoffs. Perl, for example, has XS for performance critical code, which is essentially C or C++. But the ecosystem is big enough that you don't necessarily need to write any C code yourself. And all of this is not even relevant to usability issues he tries to discuss.
  - ZenoArrow 9y ago
    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 running in under a second): http://tech.adroll.com/blog/data/2014/11/17/d-is-for-data-science.html http://tech.adroll.com/blog/data/2014/11/17/d-is-for-data-sc... It should be noted that D has a number of different compilers, offering the user the choice between compilation speed and optimisation.
ktpsns 9y ago
By the way, this is a project funded by the European Union. It got 2 Million EUR by the European Research Council (https://cordis.europa.eu/project/rcn/200802_en.html https://cordis.europa.eu/project/rcn/200802_en.html). It is only one of the many projects which give back a lot to the open source community. Thank you, EU!
- sifoo 9y ago
  I'm not quite as enthusiastic about their choice of funding target. There are plenty of other worthy languages and tools out there that could use that money better in my mind. It's the C++/Java thing all over again, but stepped up several notches; to the point where it's creeping me out since I can't even mention C online without being attacked by the Rust Brigade; and they just don't give up, it's like one of those shitty zombie movies where you have squirting body fluids and jaws chopping at you from every angle. I don't think they need any more money; more like therapy, chill pills and rooms with soft walls/locked doors for a while.
  - justinpombrio 9y ago
    This funding was for verification work, which was applied to Rust. Rust is a relatively new language, and hasn't been the focus of much research yet. C and C++, in contrast, has already been the subject of tons of research and tooling. For example, Wikipedia lists 28 static analysis tools for C, and none for Rust: https://en.wikipedia.org/wiki/List_of_tools_for_static_code_analysis#C,_C++ https://en.wikipedia.org/wiki/List_of_tools_for_static_code_... Is there a particular project for a particular language you think is promising and just needs some funding? Or does it just irk you when other people are happy? EDIT: I'm also not sure why you assume that none of this EU funding is going to your language(s) of choice; have you checked?
    - ktpsns 9y ago
      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 bugs in their parallel codes. And all codes with the "HPC" badge are parallel nowadays. I think supporting a modern ecosystem is a good decision if people move away from C++ towards Rust or Julia (another ERC... http://opendreamkit.org/ http://opendreamkit.org/). (Note: Please don't feed the trolls. Nobody has time for language rants)
crb002 9y ago
Do this at the LLVM level and you get way more languages for free.
- pcwalton 9y ago
  You can't prove safety properties of something that isn't safe. LLVM IR sure isn't.
  - haberman 9y ago
    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-untrusted-modules-at-api-level/1505/9 https://internals.rust-lang.org/t/safe-rust-sandboxing-untru... On the other hand, maybe this role is better served by WebAssembly.
    - gpm 9y ago
      Raising logic bugs from "this is maybe occasionally an annoyance, or cool piece of trivia" to "this is a security issue" seems like a bad idea in something as complex as Rust's compiler. Especially when there are many currently known bugs of this sort: https://github.com/rust-lang/rust/issues?q=is%3Aopen+is%3Aissue+label%3AI-unsound https://github.com/rust-lang/rust/issues?q=is%3Aopen+is%3Ais...
    - zzzcpan 9y ago
      I'm not sure I understand your idea, how can code generation benefit from memory safe abstractions of target languages? The whole point of code generation or rather compilation is to fit one representation into something else, doesn't matter what it is, but it has to satisfy its constraints no matter what, even if you have to use a giant global array to emulate pointers via indexes. In other words, the goal is to work around any constraints of the target language to fit yours, but not to design your language to fit any constraints of the target. Safety guarantees can only work if you carefully choose and rely on appropriate abstractions for your problem.
carapace 9y ago
> 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.
- deleted 9y ago
  [deleted]
- quotheth 9y ago
  I work for a company with a massive rust codebase. Rust is very much about building production code. What is 'good production code' ? * Few errors * Readable, well documented * Testable, has tests, has testing tools like quickcheck, fuzzing, etc * Meets performance constraints Rust hits those better than any language I've used. The downside is, oh gosh, you'll have to actually learn a programming language that isn't just another variation of the ones you learned in school.
  - carapace 9y ago
    > I work for a company with a massive rust codebase. Rust is very much about building production code. Okay, thank you, I feel a little better hearing that.
deleted 9y ago
[deleted]
p0nce 9y ago
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.
- kazagistar 9y ago
  Alternative take: upvoted comments are about the article content, while greyed out ones are people criticizing the programming language in a way that is tangentially related at best.
- Blaisorblade0 9y ago
  Rust can be criticized (https://news.ycombinator.com/item?id=16305437 https://news.ycombinator.com/item?id=16305437), but flaws will be spotted. I’ll concede nonsense on other topics might have more leeway.
vectorEQ 9y ago
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 language would write 'safer' code in rust or so. In the end it's better to learn to do things without these training wheels >.> all this hand holding is just making people weak like anything else in life.
- gliptic 9y ago
  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.
- kahnpro 9y ago
  This is a very dangerous mindset.

294 points by based2 9y ago

fovc 9y ago

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-foundations-of-the-rust-programming-language/ https://blog.acolyer.org/2018/01/18/rustbelt-securing-the-fo...

nickpsecurity 9y ago
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. stack unwinding when a panic occurs, which can cause similar issues to exception safety in C++ 4. automatic destruction, “which has already caused problems for which the Rust community still does not have a modular solution.” 5. a few details unrelated to ownership, such as type-polymorphic functions and “unsized” types.” Also shows why it’s good to have a semantics in the beginning covering the whole language like with ML or later SPARK Ada. It forces language developers to spot and address these corner cases early on. Good news is that, like with SPARK, one might just subset their use of Rust to exclusively what has been proven with no use of anything else. Is anything on the list common enough in most Rust development where it can’t be avoided and must be verified later? I’ve obviously seen many people mention traits. Arc and automatic destruction safety not being proven is a bit ironic given they’re presumably there to boost safety versus raw pointers and manual destruction. EDIT: Thanks for quick, clarifying replies about these. It's looking like a subsetting approach can work.
- dikaiosune 9y ago
  For clarification, "trait objects" are a subset of the trait system, and have much less use in rust programs than traits overall. A trait object is a dynamically dispatched pointer (often owned through Box or Arc), as opposed to the usually statically dispatched generic usage of traits that's more common in rust. Destructors aren't guaranteed to run in Rust, they aren't necessary for memory safety. It's a fair concern to note that they aren't modeled, because they are pervasive and can impact memory safety, but they don't exist to support it. Panics not being modeled is of course also a big gap, although you could always compile your code with panic=abort if you wanted to dodge that issue!
- lambda 9y ago
  You can avoid 1 if you do no multithreading, or if you accept a slower implementation of Arc. Embedded code in Rust almost always avoids 1, 2, 3, and 4. Arc is used for freeing dynamically allocated memory when all references, including across threads, are dropped, but if you're running without dynamic memory allocation, you don't need that. Trait objects also require allocation. Embedded targets also generally don't implement stack unwinding, and stack unwinding can be disabled on other targets as well; it's really only most useful in larger applications in which you want some threads to be able to continue running even if another thread panics. Automatic destruction can be fairly easily avoided if you're running without an allocator, as it is mostly used for freeing such allocated memory, as well as a few things like file handles and the like. The things covered in 5 might be harder to avoid, but also more likely to be amenable to being covered by further versions of the RustBelt work. So yes, using a subset of Rust without these features is quite feasible, and often done when working in embedded (aka no_std) code. I don't know SPARK Ada that well, but I believe it has similar constraints of no dynamic allocation. If you can do without dynamic allocation in Rust, many of the problematic features wouldn't be used.
  - dikaiosune 9y ago
    Nit: IIRC one can receive a trait object through a stack based reference. fn trait_obj(foo: &Trait)...
    - lambda 9y ago
      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 objects in an embedded context with no allocator, but I also think it's perfectly reasonable to write in a subset of Rust in which you don't use trait objects at all.
      - Argorak 9y ago
- Jweb_Guru 9y ago
  FYI, (1) is (almost) definitely being addressed in the near future.
matt_d 9y ago
Two recent talks about the project: - Derek Dreyer, Workshop on Software Correctness and Reliability 2017 (48 min): https://www.youtube.com/watch?v=Y9vemQmVeLI https://www.youtube.com/watch?v=Y9vemQmVeLI - Ralf Jung, POPL 2018 (25 min): https://plv.mpi-sws.org/rustbelt/popl18/ https://plv.mpi-sws.org/rustbelt/popl18/
- fmap 9y ago
  Derek also gave a terrific keynote talk at POPL 2018 about the big picture: https://www.youtube.com/watch?v=8Xyk_dGcAwk https://www.youtube.com/watch?v=8Xyk_dGcAwk

chrismorgan 9y ago

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 https://github.com/rust-lang/rust/issues/41622.

dmix 9y ago
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. So I'm not sure it's necessarily a 'bug' in a traditional sense that supports the use of formal verification, except in some self-serving way. That said, I'm very much in support of formal verification in these types of languages.
- rntz 9y ago
  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?
  - phkahler 9y ago
    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.
    - monocasa 9y ago
      You need to reverify when you change the code too. Otherwise you could make the same arguments about testable code.

bennofs 9y ago

Does this prove that the current borrowck rules are sufficient to catch all possible mistakes? For example, does it catch stuff like https://github.com/rust-lang/rust/issues/31287 https://github.com/rust-lang/rust/issues/31287 or https://github.com/rust-lang/rust/issues/38899 https://github.com/rust-lang/rust/issues/38899?

lambda 9y ago
What the paper demonstrates is that if you have a correct borrow checker, and you have the ability to create types using `unsafe` which can extend the semantics of the language to cover things that the borrow checker cannot cover, you can write proofs that demonstrate that the language is still sound given the addition of those types. This helps demonstrate that one of the fundamental design goals of Rust, have a simple but limited system of borrowing built into the language, and allow more complex forms of managing reference types safely built on top of it as library features using `unsafe`, is a fundamentally sound design. In other words, you don't have to treat the language and all libraries using `unsafe` as one large system that you need to prove soundness of, but you can do modular proofs of the core language, and each library that adds a new type of memory and reference management, independently. Those bugs you reference are simply bugs in Rust's borrow checker. The language used for the RustBelt paper, LambdaRust, is a language that is much simpler than Rust itself, making the borrow checking much easier but the language not as convenient to use (it is not intended to be used at all, just to act as a model of Rust). The things you reference are simply bugs, but because of the fairly expressive syntax that Rust offers actually getting the borrow checker right can be be difficult in some cases. I don't think that there are any theoretical concerns about the ability to write a correct borrow checker, just practical issues with the current implementation not correctly handling certain cases.
- bennofs 9y ago
  > I don't think that there are any theoretical concerns about the ability to write a correct borrow checker, just practical issues with the current implementation not correctly handling certain cases. Is it really that trivial? When looking through https://github.com/rust-lang/rust/blob/master/src/librustc_borrowck/borrowck/README.md https://github.com/rust-lang/rust/blob/master/src/librustc_b..., it is not at all clear that these rules cover everything to me. There are some complex side conditions, isn't it easy to miss something there?

Asdfbla 9y ago

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 methods now find more practical application, so it's easier to get people (who aren't hardcore logicians) interested in the whole topic.

dtornabene 9y ago
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.
pornel 9y ago
I find Rust's RFC/design discussions fascinating. They're a mix of serious Programming Language Theory and practice. The same feature in Rust is seen by some as "algebraic data types" and "oh cool, I can add data to enums" by others. Some feature proposals starting with "wouldn't it be nice to have…" end up designed with input from people who literally have a PhD in this feature (and are bikesheded until people without PhDs can use the feature).

nukeop 9y ago

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, unfriendly, constrained, unappealing, etc. of all of them. Warnings and errors appeared systematically and, despite their verbosity, were rarely helpful. 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. Being so concerned about making sure that the generated code is extremely safe no matter what by sacrificing flexibility and user friendliness is far from ideal. Restrictions and prohibitions have always to be seen as an in-the-worst-case-scenario resource, not as a primary solution; much less when dealing with something as complex as programming, a very powerful tool supposed to be managed by knowledgeable individuals. The higher the freedom, the better the results delivered by a sensible/knowledgeable person. Unless Rust changes a lot, I don't see it going anywhere. It might get some support from theoretical/academical/inside-whatever-bubble circles, but seriously doubt that developers with real-world experience can like or even accept most of what this language represents.

mkesper 9y ago
Rust is a direct contender to C and C++, not to script or GC languages. Please compare apples to apples.
- zzzcpan 9y ago
  Only for some code it's not apples to apples. For most code GC is not a big deal and the languages just offer different tradeoffs. Perl, for example, has XS for performance critical code, which is essentially C or C++. But the ecosystem is big enough that you don't necessarily need to write any C code yourself. And all of this is not even relevant to usability issues he tries to discuss.
- ZenoArrow 9y ago
  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 running in under a second): http://tech.adroll.com/blog/data/2014/11/17/d-is-for-data-science.html http://tech.adroll.com/blog/data/2014/11/17/d-is-for-data-sc... It should be noted that D has a number of different compilers, offering the user the choice between compilation speed and optimisation.

ktpsns 9y ago

By the way, this is a project funded by the European Union. It got 2 Million EUR by the European Research Council (https://cordis.europa.eu/project/rcn/200802_en.html https://cordis.europa.eu/project/rcn/200802_en.html). It is only one of the many projects which give back a lot to the open source community. Thank you, EU!

sifoo 9y ago
I'm not quite as enthusiastic about their choice of funding target. There are plenty of other worthy languages and tools out there that could use that money better in my mind. It's the C++/Java thing all over again, but stepped up several notches; to the point where it's creeping me out since I can't even mention C online without being attacked by the Rust Brigade; and they just don't give up, it's like one of those shitty zombie movies where you have squirting body fluids and jaws chopping at you from every angle. I don't think they need any more money; more like therapy, chill pills and rooms with soft walls/locked doors for a while.
- justinpombrio 9y ago
  This funding was for verification work, which was applied to Rust. Rust is a relatively new language, and hasn't been the focus of much research yet. C and C++, in contrast, has already been the subject of tons of research and tooling. For example, Wikipedia lists 28 static analysis tools for C, and none for Rust: https://en.wikipedia.org/wiki/List_of_tools_for_static_code_analysis#C,_C++ https://en.wikipedia.org/wiki/List_of_tools_for_static_code_... Is there a particular project for a particular language you think is promising and just needs some funding? Or does it just irk you when other people are happy? EDIT: I'm also not sure why you assume that none of this EU funding is going to your language(s) of choice; have you checked?
  - ktpsns 9y ago
    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 bugs in their parallel codes. And all codes with the "HPC" badge are parallel nowadays. I think supporting a modern ecosystem is a good decision if people move away from C++ towards Rust or Julia (another ERC... http://opendreamkit.org/ http://opendreamkit.org/). (Note: Please don't feed the trolls. Nobody has time for language rants)

crb002 9y ago

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

pcwalton 9y ago
You can't prove safety properties of something that isn't safe. LLVM IR sure isn't.
- haberman 9y ago
  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-untrusted-modules-at-api-level/1505/9 https://internals.rust-lang.org/t/safe-rust-sandboxing-untru... On the other hand, maybe this role is better served by WebAssembly.
  - gpm 9y ago
    Raising logic bugs from "this is maybe occasionally an annoyance, or cool piece of trivia" to "this is a security issue" seems like a bad idea in something as complex as Rust's compiler. Especially when there are many currently known bugs of this sort: https://github.com/rust-lang/rust/issues?q=is%3Aopen+is%3Aissue+label%3AI-unsound https://github.com/rust-lang/rust/issues?q=is%3Aopen+is%3Ais...
  - zzzcpan 9y ago
    I'm not sure I understand your idea, how can code generation benefit from memory safe abstractions of target languages? The whole point of code generation or rather compilation is to fit one representation into something else, doesn't matter what it is, but it has to satisfy its constraints no matter what, even if you have to use a giant global array to emulate pointers via indexes. In other words, the goal is to work around any constraints of the target language to fit yours, but not to design your language to fit any constraints of the target. Safety guarantees can only work if you carefully choose and rely on appropriate abstractions for your problem.

carapace 9y ago

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

deleted 9y ago
[deleted]
quotheth 9y ago
I work for a company with a massive rust codebase. Rust is very much about building production code. What is 'good production code' ? * Few errors * Readable, well documented * Testable, has tests, has testing tools like quickcheck, fuzzing, etc * Meets performance constraints Rust hits those better than any language I've used. The downside is, oh gosh, you'll have to actually learn a programming language that isn't just another variation of the ones you learned in school.
- carapace 9y ago
  > I work for a company with a massive rust codebase. Rust is very much about building production code. Okay, thank you, I feel a little better hearing that.

deleted 9y ago

[deleted]

p0nce 9y ago

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.

kazagistar 9y ago
Alternative take: upvoted comments are about the article content, while greyed out ones are people criticizing the programming language in a way that is tangentially related at best.
Blaisorblade0 9y ago
Rust can be criticized (https://news.ycombinator.com/item?id=16305437 https://news.ycombinator.com/item?id=16305437), but flaws will be spotted. I’ll concede nonsense on other topics might have more leeway.

vectorEQ 9y ago

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 language would write 'safer' code in rust or so. In the end it's better to learn to do things without these training wheels >.> all this hand holding is just making people weak like anything else in life.

gliptic 9y ago
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.
kahnpro 9y ago
This is a very dangerous mindset.