3 ms·

> I believe that type checking should closely match the reasoning programmers do in their head, and thereby verify the correctness of that reasoning. Conversely

by lmm 3y ago

> I believe that type checking should closely match the reasoning programmers do in their head, and thereby verify the correctness of that reasoning. Conversely, this means that programmers must express their reasoning through the type system. If something doesn’t typecheck, either the reasoning as expressed is wrong or incomplete, or the programmer has used some reasoning that cannot be expressed in the type system (meaning that the type system is lacking in that respect). Right. The (well, a) problem with NLL in Rust is that it isn't expressible; it creates lifetimes that don't correspond to anything in the syntax, and so can't be written explicitly into the program even if the programmer wants to. (As opposed to conventional type inference where you can always write the type explicitly if the code is confusing)

Rusky 3y ago
You couldn't write explicit lifetimes before NLL, either. (Nor does conventional type inference mean you can always write the type! This is why people who design type systems care about "principal types.") NLL (and even moreso Polonius) brought the borrow checker closer to how programmers reason about lifetimes in their head than it was before, empirically speaking. The thing you described was a worry at the time but it never turned out to be accurate. If there is anything about the borrow check that does match your description, it is things like "borrow splitting" and mutable reborrows, which can be done locally but are not expressible in function signatures. These problems existed long before NLL, though, and don't have anything to do with syntax or lexical scope.
- lmm 3y ago
  > You couldn't write explicit lifetimes before NLL, either. Well, no, but you can write scopes explicitly, and all your lifetimes correspond to scopes, by definition. > NLL (and even moreso Polonius) brought the borrow checker closer to how programmers reason about lifetimes in their head than it was before, empirically speaking. The thing you described was a worry at the time but it never turned out to be accurate. It worked for how some programmers reason about lifetimes in their head. Not for me. Maybe I'm the minority.

by lmm 3y ago

Rusky 3y ago

You couldn't write explicit lifetimes before NLL, either. (Nor does conventional type inference mean you can always write the type! This is why people who design type systems care about "principal types.") NLL (and even moreso Polonius) brought the borrow checker closer to how programmers reason about lifetimes in their head than it was before, empirically speaking. The thing you described was a worry at the time but it never turned out to be accurate. If there is anything about the borrow check that does match your description, it is things like "borrow splitting" and mutable reborrows, which can be done locally but are not expressible in function signatures. These problems existed long before NLL, though, and don't have anything to do with syntax or lexical scope.

lmm 3y ago
> You couldn't write explicit lifetimes before NLL, either. Well, no, but you can write scopes explicitly, and all your lifetimes correspond to scopes, by definition. > NLL (and even moreso Polonius) brought the borrow checker closer to how programmers reason about lifetimes in their head than it was before, empirically speaking. The thing you described was a worry at the time but it never turned out to be accurate. It worked for how some programmers reason about lifetimes in their head. Not for me. Maybe I'm the minority.