5 September 2021

The future of typed computing

TL;DR

• Conversely to enabling programmers to express more programs, there is an effort on improving guarantees by allowing programmers to tighten up the guarantees.
• It's achieved by introducing dependent types, which are, in essense, systems that allow you to write functions over types themselves.
• Furthermore, special kind of types that ensure that every value is used exactly once or not more than once are possible. They are called linear and affine types.
• These types are collectively called "substructural types" and stem from substructural logic.
• These types power ownership, move semantics and borrow checking in Rust.
• In Rust, affinity is not exposed to the end users.
• The only industrial language with affine and linear types exposed to the users is Haskell.
• Substructural types enable more proceedings in type systems.
• There are formal methods for reasoning about distributed computing based on process calculi.
• Compared to Turing machines, most of lambda calculi and most other models of computation, process calculi are *not* sequential.
• Type system engineering adopts it via something called "session types".
• types enable something called "session types", which are likely to back the type systems popularity of microservices and distributed frameworks like Akka and Erlang systems demonstrate the power of concurrent and parallel programming.