Thomas Fischbacher wrote:
> He presumably wanted to see a different thing, e.g. 
> automatically transforming

> let rec fac1 x =
>   if x = 0
>   then 1
>   else x*(fac1 (x-1))
> ;;
> 
> into
> 
> let fac2 x =
>   let rec walk so_far todo =
>     if todo = 0
>     then so_far
>     else walk (todo*so_far) (todo-1)
>   in walk 1 x
> ;;
> 
> My impression is that it may indeed be possible to do something like this 
> for simple applications, but that the cases that can be covered 
> automatically presumably are so limited that an experienced programmer 
> will usually want to attack them by going to a higher form of abstraction 
> and not waste time on such things anyway.

Incidentally, I recently wrote a little piece on how to transform one
kind of recursion into another kind of recursion via
propositions-as-types http://math.andrej.com/2005/09/16/proof-hacking/
which may be of interest to some of you. I only considered a very simple
kind of recursion on natural numbers. My impression is that quite a
general form of recursion could be treated (replace natural numbers by a
well-founded type, for example).

This sort of thing is probably not immediately useful in programming
practice. But even "real" programmers should be aware of abstract
mathematical ideas because they they indirectly make them write better
programs.

Best regards,

Andrej