[Haskell-cafe] Compiler's bane

[Brandon S. Allbery KF8NH]

On 2008 Sep 1, at 20:06, Tillmann Rendel wrote:
> Andrew Coppin wrote:
>> 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.


You can define a set of valid transformations, have the interpreter  
log each transformation, and verify that all are correct (that is,  
that both the transformation and the logged result are correct.

This assumes the interpreter can be resolved down to a sufficiently  
simple set of transformations; if not, you're right back at having the  
tester being the interpreter itself.  Note that you don't check if the  
transformation plan for the program matches a specified list, just  
that all transformations are correct.  (Just remember that "logic is  
an organized way of going wrong with confidence.")

-- 
brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery at kf8nh.com
system administrator [openafs,heimdal,too many hats] allbery at ece.cmu.edu
electrical and computer engineering, carnegie mellon university    KF8NH