[Agda] Re: Agda running in the browser

[Jesper Louis Andersen]

On Sat, Sep 17, 2011 at 13:40, Conor McBride <conor at strictlypositive.org> wrote:

> Remember, "Agda is total, so it can't be Turing Complete" is as
> much nonsense as saying "Haskell is pure so it can't do IO".

Totality is many things. In practice you just have a step function,
and choose the amount of steps to be larger than the lifetime of the
universe. Isn't this a total program? It provably terminates after K
steps, (K incomprehensibly large). So our program will be known to
behave on this side of Ragnarok.

I guess you could try to wiggle a path through coinduction, but I saw
the above trick used by Xavier Leroy in some Coq developments he did.

-- 
J.