[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
While there are several works providing support to discipline channel
communication in Rust, based on (Multi-party) Session Types, there is a
lack of support to discipline the protocols of modules (seen as APIs).
José Duarte and I developed a DSL to provide typestate support for Rust.
We recently had a paper accepted in the Brazilian Symposium of
Programming Languages (proceedings published in the ACM DL):
http://cbsoft2021.joinville.udesc.br/sblp.php
You can find the paper here:
https://github.com/rustype/typestate-rs/tree/main/paper
The software is also already available:
https://lib.rs/crates/typestate-proc-macro
Comments most welcome.
--
Cheers,
António
(also on behalf of José)
-----------------------
Abstract:
Rust leverages the type system along with information about object
lifetimes, allowing the compiler to keep track of objects throughout the
program and checking for memory misusage. While preventing
memory-related bugs goes a long way in software security, other
categories of bugs remain in Rust. One of which would be Application
Programming Interface (API) misusage, where the developer does not
respect constraints put in place by an API, thus resulting in the
program crashing.
Typestates elevate state to the type level, allowing for the enforcement
of API constraints at compile-time, relieving the developer from the
burden that is keeping track of the possible computation states at
runtime, and preventing possible API misusage during development. While
Rust does not support typestates by design, the type system is powerful
enough to express and validate typestates.
We propose a new macro-based approach to deal with typestates in Rust;
this approach provides an embedded Domain-Specific Language (DSL) which
allows developers to express typestates using only existing Rust syntax.
Furthermore, Rust’s macro system is leveraged to extract a state machine
out of the typestate specification and then perform compile-time checks
over the specification. Afterwards we leverage Rust’s type system to
check protocol-compliance. The DSL avoids workflow-bloat by requiring
nothing but a Rust compiler and the library itself.
