Greg WilsonAn E-Bike for the Mind: https://third-bit.com/2026/03/28/e-bike-for-the-mind/
Speaking of which, do any of my programming language friends know of a type system that captures "how it's used" as opposed to "what values it's allowed to have" in the way that Sajaniemi's variable roles do? Borrow checking in Rust is kind of somewhat adjacent, but not really the same thing - any others?
Sylvain Soliman ☕️@gvwilson Haven't read your above article, but I'd say that in languages, like Prolog, which is usually not typed, and has both a notion of failure and a separate notion of error/exception, when you add a type system it's often _descriptive_ rather than _prescriptive_, which seems related to the question you're asking…
The question being how would you want to type:
```
append([], L, L).
append([H|T], L, [H|M]) :- append(T, L, M).
```
since the first clause would _succeed_ with any `L`.