[TYPES] Systematically testing type systems

[Matthias Felleisen]

On Jul 4, 2006, at 6:13 AM, Klaus Ostermann wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ 
> types-list ]
>
> Hi all,
>
> I hope this is not a stupid question, but I wonder whether it is  
> feasible to
> test the soundness of a type checker by enumerating all programs in  
> the
> language, reducing each program one step (assuming we have a small- 
> step
> interpreter and a language where the full execution state is in the  
> program
> itself) and checking whether subject reduction holds. If the  
> enumeration of all
> programs would be smart enough (i.e., produce only syntactically  
> correct
> programs; no two programs in the enumeration are alpha-equivalent)  
> I could
> imagine that it would be feasible to test a type checker for all  
> programs less
> than X bytes in size, where X is a reasonable number (e.g., 1KB) -  
> at least for
> minimalistic languages as they are common in type research.
>
> Has this ever been tried, or is it obvious that it would not work  
> in practice?

That was one of the goals behind our PLT Redex tool (see RTA 2004,  
Aachen): test then verify.

It's not quite there yet. I can imagine that the performance of a  
well-tuned logic-based system, such as the early INRIA efforts, could  
be better.

-- Matthias