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

Brendan Zabarauskas

@brendanzab

Feb 28, 2021

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.

ᵉᵈᵈʸᵇ

@eddyb_r

Feb 28, 2021

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

Replying to

and

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.

3:03 AM · Feb 28, 2021Twitter Web App

Replying to

and

I guess Rust with refinement types could do a bit more, such as partial borrowing a subset of fields, variant types, etc. but it still only gets you a bit farther

ᵉᵈᵈʸᵇ

@eddyb_r

Feb 28, 2021

personally I probably want to always work with a hybrid model of immutable graph-shaped computation with isolated pockets using short-lived linear/affine data structures (as optimizations over the equivalent immutable-only algorithms) oh, btw, rustc is a bit like this already!

Show replies