[TYPES] Systematically testing type systems

[David Hopwood]

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?

It is obvious that it would not work in practice for programs up to 1 Kbyte.
It could only work for programs up to a few tokens in length.

-- 
David Hopwood <david.nospam.hopwood at blueyonder.co.uk>