Thanks for these links!

Austral rational documentation is indeed really interesting. My preference goes into another direction (notably toward expression-based languages), but it's refreshing to read well explained design decisions.

The section about linear types is also a gem to this regard. I would even consider this as a reference source to introduce the motivations and principles behind the Rust type system and borrow checker. Only the syntax would have to be made a bit more rusty.

[1] https://austral-lang.org/spec/spec.html#rationale-linear-typ...