[TYPES] Systematically testing type systems

[Klaus Ostermann]

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?

Klaus Ostermann