A Transient Semantics for Typed Racket
Ben Greenman 
, Lukas Lazarek, Christos Dimoulas, and Matthias Felleisen
(Brown University, USA; Northeastern University, USA; Northwestern University, USA)
Mixed-typed languages enable programmers to link typed and untyped components
in various ways. Some offer rich type systems to facilitate the smooth
migration of untyped code to the typed world; others merely provide a
convenient form of type Dynamic together with a conventional structural type
system. Orthogonal to this dimension, Natural systems ensure the integrity of
types with a sophisticated contract system, while Transient systems insert
simple first-order checks at strategic places within typed code. Furthermore,
each method of ensuring type integrity comes with its own blame-assignment
strategy.
Typed Racket has a rich migratory type system and enforces the types with a
Natural semantics. Reticulated Python has a simple structural type system
extended with Dynamic and enforces types with a Transient semantics. While
Typed Racket satisfies the most stringent gradual-type soundness properties at
a significant performance cost, Reticulated Python seems to limit the
performance penalty to a tolerable degree and is nevertheless type sound. This
comparison raises the question of whether Transient checking is applicable to
and beneficial for a rich migratory type system.
This paper reports on the surprising difficulties of adapting the Transient
semantics of Reticulated Python to the rich migratory type system of Typed
Racket. The resulting implementation, Shallow Typed Racket, is faster than the
standard Deep Typed Racket but only when the Transient blame assignment
strategy is disabled. For language designers, this report provides valuable
hints on how to equip an existing compiler to support a Transient semantics.
For theoreticians, the negative experience with Transient blame calls for a
thorough investigation of this strategy.
@InProceedings{Programming Journal, Volume22p102,
author = {Ben Greenman and Lukas Lazarek and Christos Dimoulas and Matthias Felleisen},
title = {A Transient Semantics for Typed Racket},
booktitle = {Proc.\ Programming Journal, Volume},
publisher = {AOSA},
pages = {102--127},
doi = {10.22152/programming-journal.org/2022/6/9},
year = {2022},
}
Publisher's Version
Automated, Targeted Testing of Property-Based Testing Predicates
Tim Nelson, Elijah Rivera, Sam Soucie, Thomas Del Vecchio, John Wrenn, and Shriram Krishnamurthi
(Brown University, USA; Massachusetts Institute of Technology, USA; Indiana University, USA)
Context This work is based on property-based testing (PBT). PBT is an increasingly important form of software testing. Furthermore, it serves as a concrete gateway into the abstract area of formal methods. Specifically, we focus on students learning PBT methods.
Inquiry How well do students do at PBT? Our goal is to assess the quality of the predicates they write as part of PBT. Prior work introduced the idea of decomposing the predicate’s property into a conjunction of independent subproperties. Testing the predicate against each subproperty gives a “semantic” understanding of their performance.
Approach The notion of independence of subproperties both seems intuitive and was an important condition in prior work. First, we show that this condition is overly restrictive and might hide valuable information: it both undercounts errors and makes it hard to capture misconceptions. Second, we introduce two forms of automation, one based on PBT tools and the other on SAT-solving, to enable testing of student predicates. Third, we compare the output of these automated tools against manually-constructed tests. Fourth, we also measure the performance of those tools. Finally, we re-assess student performance reported in prior work.
Knowledge We show the difficulty caused by the independent subproperty requirement. We provide insight into how to use automation effectively to assess PBT predicates. In particular, we discuss the steps we had to take to beat human performance. We also provide insight into how to make the automation work efficiently. Finally, we present a much richer account than prior work of how students did.
Grounding Our methods are grounded in mathematical logic. We also make use of well-understood principles of test generation from more formal specifications. This combination ensures the soundness of our work. We use standard methods to measure performance.
Importance As both educators and programmers, we believe PBT is a valuable tool for students to learn, and its importance will only grow as more developers appreciate its value. Effective teaching requires a clear understanding of student knowledge and progress. Our methods enable a rich and automated analysis of student performance on PBT that yields insight into their understanding and can capture misconceptions. We therefore expect these results to be valuable to educators.
@InProceedings{Programming Journal, Volume22p128,
author = {Tim Nelson and Elijah Rivera and Sam Soucie and Thomas Del Vecchio and John Wrenn and Shriram Krishnamurthi},
title = {Automated, Targeted Testing of Property-Based Testing Predicates},
booktitle = {Proc.\ Programming Journal, Volume},
publisher = {AOSA},
pages = {128--156},
doi = {10.22152/programming-journal.org/2022/6/10},
year = {2022},
}
Publisher's Version
Info