Programming Languages

Another post from the creator of Vale, the last one was "Borrow checking, RC, GC, and the Eleven (!) Other Memory Safety Approaches".

This discusses Vale's higher RAII, a feature implemented using linear types. Vale has linear types as opposed to Rust's affine types: affine types prevent using a value after it's "moved", but linear types also prevent not moving a value (i.e. cannot just let it go out of scope). Additionally in Vale, one can define a set of functions that destroy a type, and in order to destroy a value of that type, one must call a function from that set; that is what Vale calls "higher RAII".

This part of the linked post contains seven examples where Vale's higher RAII enforce invariants that Rust's affine types cannot. In a language like C, you can "forget" to use a value and it will leak. In a language like Rust, the value will be properly deallocated, but you can still have "forgotten" about it, e.g. perhaps the value represents a transaction that you meant to commit (one of the seven examples). In Vale, you can't forget about a value as long as it has a linear type, because doing so will raise a compile-time error.

The rest of the post further discusses higher RAII, elaborating on what it is and why its useful, explaining why it's more general than other languages' defer and how it could be integrated into other languages, and more.