Conversation

ᵉᵈᵈʸᵇ
@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
ᵉᵈᵈʸᵇ
@eddyb_r
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
1
1
Brendan Zabarauskas
@brendanzab
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.
1
4
ᵉᵈᵈʸᵇ
@eddyb_r
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
1
2
ᵉᵈᵈʸᵇ
@eddyb_r
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!
2
2
Brendan Zabarauskas
@brendanzab
Yeah I've been interested in graph and hypergraph stuff - more from a user-oriented perspective. Like, doing dependencies in types and terms nicely, allowing for out of order declarations/definitions of fields/parameters, etc.
1
1
Brendan Zabarauskas
@brendanzab
Like, trying to get away from the positionalness that seems to pervade a great deal of type theory (eg. currying etc). I think having proper support for named graphs would be super nice from a user perspective.
1
2
Brendan Zabarauskas
@brendanzab
But yeah, I stuggle because I'm really not good at graph stuff, and I need to somehow come up with a type checking and efficient normalization/conversion algorithm for it if I want to actually use it in my type checker.
1
2