The following blog post is referenced in the proposal: https://www.tweag.io/blog/2017-08-03-linear-typestates/ https://www.tweag.io/blog/2017-08-03-linear-types

The following blog post is referenced in the proposal: https://www.tweag.io/blog/2017-08-03-linear-typestates/ https://www.tweag.io/blog/2017-08-03-linear-typestates/ . This is maybe a different aspect than what others have been trying to explain, but I found the socket-based example enlightening. Type states allow the state of the socket (unbound, bound, listening, closed) to be expressed as a part of the type (a type annotation, if you will) so the compiler can verify that you're not reusing a closed socket, or try to send data over an unbound socket. Linear types then, allow to express in code how a type (annotation) changes over time (e.g., "bind() takes an unbound socket and returns it an a bound state") so the compiler can statically check that it's in a valid state for every operation.