[Agda] Pie in the sky

[Benja Fallenstein]

Hi Samuel,

On Sat, Sep 25, 2010 at 7:22 AM, Samuel Gélineau <gelisam at gmail.com> wrote:
> I find it funny that we're working in a language where every function
> has to pass a termination checker, yet each language extension gets
> scrutinized to make sure they are terminating. Somebody should write a
> provably-terminating Agda compiler in Agda; this would make it much
> easier to ensure that further language extensions preserve
> termination.

Yes, but since an Agda type checker needs to normalize arbitrary Agda
code, this isn't *trivial* (there's some potentially relevant work by
Turing, Gödel and Tarski) :-)

I'm hoping that similarly to how we can prove

ZFC |- Inacc -> con(ZFC),

it would be possible to write a function

agda : X -> CompilerInput -> Maybe CompilerOutput

where X is a suitable axiom -- a universe construction? a large ordinal?

Hopefully there is a construction of this sort that will seem the most
perfectly natural thing in the world once we have it written down, but
my point is, the task is not quite as trivial as "just switch the
implementation language from Haskell to Agda"...

All the best,
- Benja