I think the big innovations in Rust are borrowing and the integration with unsafe. It's precisely the approach to unsafe that's crucial and also less ambitious than a system trying to do everything in safe code.
-
-
Replying to @samth @johnregehr and
Less ambitious in one sense, since it allows you to use the full power of higher order separation logic (which no one is trying to claim is a usable general purpose programming language) in proving the unsafe specs. But it also means a more complicated semantic typing model.
1 reply 0 retweets 0 likes -
Replying to @awesomeintheory @johnregehr and
I don't think it's right to say that Rust itself features higher-order separation logic, in the same way that the ML module system doesn't actually have translucent sums. The less ambitious part is that you just write `unsafe` and don't prove anything!
1 reply 0 retweets 0 likes -
Replying to @samth @johnregehr and
Well, sure, but we are actually trying to prove things :)
1 reply 0 retweets 0 likes -
Replying to @awesomeintheory @samth and
And, I think the fact that there *is* a semantic model that seems (1) to mostly correspond to Rust's type system, (2) be formalizable in Coq, (3) be strong enough to show that a bunch of existing unsafe code is correct, is a pretty major advance in the state of the art.
1 reply 0 retweets 3 likes -
Replying to @awesomeintheory @johnregehr and
Right, _you_ are trying to prove things. I think the novelty and ambition of the RustBelt work is quite clear, and I would be surprised if anything like that had the same difficulties getting accepted that papers on the design of Rust had.
1 reply 0 retweets 0 likes -
Replying to @samth @johnregehr and
That's fair, but a lot of what we're doing is just translating over concepts that are already baked into the language design. A lot of these specs wouldn't be type-able in other general purpose languages. So I don't think you can cleanly separate RustBelt from the design of Rust.
1 reply 0 retweets 0 likes -
Replying to @awesomeintheory @johnregehr and
That's true, but I also think it answers neither the question "why does rust work when cyclone etc don't" nor "why was a design paper on rust hard to publish".
2 replies 0 retweets 0 likes -
Replying to @samth @awesomeintheory and
My sense is that academia thought substructural type systems were a dead end at the time, and it was going to be very hard to get anything about them published no matter what. It’s just the sense I had though; could be wrong.
1 reply 0 retweets 0 likes -
I think academics may have a tendency to think that if ideas don’t catch on in practice that it’s because they’re inherently flawed. But in many (most?) cases failure to achieve industry success is due to poor execution or just bad luck, not because of the ideas.
6 replies 4 retweets 18 likes
The one decent review we got for the Rust paper basically said “well, substructural type systems are a failed idea, but people seem to be actually writing a lot of code in this language, so this is intriguing”
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.