Conversation

Overall a thing that is going to be a problem for me with Rust is A thing I want: A language with linear types What Rust is: A language which type-enforces only a single mutable pointer to any buffer, internally using a linear typing engine A thing I don't want: That

ᵉᵈᵈʸᵇ

@eddyb_r

Feb 28, 2021

I don't really understand this take, tbh all of the mutability rules are so *you can have a typesystem* without those rules, it gets *really easy* (and there have been subtle soundness bugs that have allowed this to happen in the past!) to corrupt values in safe code

ᵉᵈᵈʸᵇ

@eddyb_r

Feb 28, 2021

most of the advanced typesystems are in completely-mutation-free functional programming land, *and for good reason* mutation-at-a-distance is effectively the ability to corrupt anyone else's view of the data you can get around this with GC, but your types can't be too fancy

ᵉᵈᵈʸᵇ

@eddyb_r

Feb 28, 2021

Rust *is the first language* that fits all 3 of: 1. no GC 2. can trust types, in that values won't get become invalid behind your back 3. you don't have to write heavy proofs of this yourself, but can instead rely on correct-by-construction IIRC F* may have 1+2 but not 3

Replying to

and

Also F* requires you to write code in a restricted subset of the language (Low*) if you want 1 😟 - it's nice that Rust lets you have a highish level of language that automates a bunch of this lowering you'd otherwise need to do by hand.

2:59 AM · Feb 28, 2021Twitter Web App

Replying to

and

Would be interested to know how far Cogent got with this stuff 🤔

Replying to

and

would you agree that it's hard to do much better than Rust without some kind of global analysis? like there is a fundamental limit to how much you can handle with just local reasoning, right? e.g. I had some ideas for Cell::with_mut that require global callgraph checks to work

Brendan Zabarauskas

@brendanzab

Feb 28, 2021

I'm not sure… probably? I think it would be neat if a language let you do more with separation logic directly, but that would probably require more work from the programmer, with less of the automation the Rust's type system provides.

Show replies