[Agda] Size limit on generated code?

[Peter Hancock]

On 27/09/2014 13:08, Andreas Abel wrote:
> Haha, these are truly insane numbers! 

I found this discussion, and the horrific numbers most interesting. A natural reaction is
that there must be a (hugely) better way of producing an executable.   I'm sure a lot
of worthwhile thought has gone into producing good executables from haskell code; but
jamming agda into haskell and relying on haskell to make something sensible out of it seems
distictly over-optimistic.  We're at run-time, and we might as well be in untyped lambda calculus,
or combinators.

Or is it (also?) that we want to make use of Haskell's IO-monad?

If there are now 3 sort-of backends for producing executables, there is probably something like
an interface between what the type-checker passes on to the code generator, or a rough idea of what
it might be.  Are there papers, or code modules, where I can learn something about what people think?

I spoke a week ago to someone currently at Microsoft who has experience with functional languages,
and LLVM , who claims to be at a loose end, and dying to get their teeth into something juicy.

The issue of the IO interface is maybe a subtle one.  An executable agda program is, in my dreams,
a thing that (when executed) does something, intertwined with proofs that the effect its execution will
have on the world meets a specification (expressed in terms of state-predicate transformers, or some such foundation).  A lot of the "proofs" might not be run-time-relevant, if the run-time system is to trust the type-checker.  (But it may be relevant to the prosecution of guilty parties when some airplane falls out of
the sky.)

Hank