[Haskell-cafe] Compiler's bane

[Tillmann Rendel]

Andrew Coppin wrote:
> Here is a *much* bigger problem: How do you check that an interpretter 
> is correct??

Before checking for correctness, you have to define correctness. What is 
the specification of your interpreter?

> You can't very easily write a QuickCheck property that will generate 
> every possible valid expression and then check that the output of the 
> interpretter is formally equivilent. The QuickCheck property would be a 
> second copy of the interpretter, which proves nothing!

Well, if you have two *different* interpreters, that would at least 
reassure you somewhat. Consider a naive substituation-based interpreter 
and a clever environment-based interpreter. The former is often easier 
to write and easier to get correct, and the latter is often what you 
want in the end.

Since you seem to be implementing a standard language, you could use an 
existing implementation to check against. many lambda calculus style 
languages can easily be transformed into scheme, for example.

> Any hints? Just how *do* you check something large like this?

You could write a lot of test cases, calculating the correct answers by 
hand.

You could check that during evaluation, you have always wellformed terms 
(e.g. evaluation does not introduce new free variables). You could even 
check that after evaluation stops, you have indeed a normal form.

You could try to check the components of your interpreter (e.g. 
environment lookup, term substituation, simplification) independently.

   Tillmann