Conversation

mcc
@mcclure111
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
5
17
ᵉᵈᵈʸᵇ
@eddyb_r
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
1
6
ᵉᵈᵈʸᵇ
@eddyb_r
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
2
7
ᵉᵈᵈʸᵇ
@eddyb_r
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
1
7
Brendan Zabarauskas
@brendanzab
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
4