Well, sure, but we are actually trying to prove things :)
Conversation
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
3
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
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
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
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
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
5
18
I don't agree with the first part of this take-- academics can create whole communities, running for decades, with very little adoption in practice of the ideas
3
11
Yeah, maybe it more has to do with having a champion in the field. Substructural type systems didn’t seem to have many champions in academia when Rust came on the scene.
1
which means you faced this uphill battle, which sucks. but once this energy barrier is overcome, subsequent papers have a much easier time.
2
3
Yeah, I'm super excited about all the substructral and modal type system work coming out now in the PL research world. Rust has made a big impact in helping to bring it back into vogue and I'm thankful for it!