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.
-
-
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 -
Replying to @pcwalton @awesomeintheory and
My theory is that many ideas are first proposed in too strong a form (a safe programming language with manual memory management! a type checker that works for any scheme code! a partial evaluator that generates a compiler!) and success is in scaling back to something workable.
2 replies 0 retweets 7 likes -
But those scaled-back systems are harder to publish initially because they are, in a real sense, doing less than was originally proposed. And those examples all got published at not-top venues initially, and then became a big deal.
1 reply 0 retweets 3 likes -
Replying to @samth @awesomeintheory and
This actually applies to Pathfinder too. It’s in many ways a scaled-back version of “Massively Parallel Vector Graphics” (though I developed it independently and only later realized the connection). It seems to outperform MPVG, ironically, because it’s so scaled-back.
2 replies 0 retweets 0 likes -
MPVG does everything on GPU using compute and CUDA; Pathfinder uses the standard GPU pipeline and punts some work to CPU. (This also allows more parallelism—might as well use the CPU since it’s there!) Also, MPVG uses a complicated hierarchy of tiles; PF is a uniform grid.
-
-
0 replies 0 retweets 2 likesThanks. Twitter will use this to make your timeline better. UndoUndo
-
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.