Proofs and development

[Adrian Hey]

On Tue 02 Jun, Marko van Eekelen wrote:
> /* Automatically proven theorems */
> T18 [a:SET] [x:List a] Reverse (Reverse x) = x

This looks very interesting. I'm sure we've all faced the difficult choice
of 'simple but inefficient definition' vs. 'complex but efficient algorithm'.
If it would be very useful if we could prove their equivalence. I'm a little
curious about one thing though. As most functional programming enthusiasts
will be aware, you need to be a bit careful when reasoning about lazy
languages. For example, despite T18 above, in a real Clean program...

   Reverse (Reverse [1,2..]) = _|_,    which isn't equivalent to [1,2..]

Have you decided what implications this has for the use of this kind of
theorem prover with Clean, or is it too early to ask this question?

Regards
-- 
Adrian Hey