[Submitted on 5 Jan 2023]
Abstract: Advanced type systems that enforce various correctness and safety
guarantees–such as linear and ownership types–have a long history in the
Programming Languages research community. Despite this history, a
human-centered evaluation of these type systems and their usability was all but
absent, with empirical evaluations limited to testing their expressiveness in
programs written by experts, i.e. the cre
