The Coq mailing list

[David von Oheimb <oheimb AT informatik.tu-muenchen.de>]

Good afternoon Steve,

>         I'm contemplating extensions to functional languages that
> would support development of formal projects like provers. 

I guess you mean facilities that can be used to "shallow embedd" certain
technical components of provers. Would be nice, but I suppose that such
extensions, similarly to (or even worse than) general library solutions,
won't be flexible enough: How could user code modify such facilities,
e.g. by adding A/C matching, or explicit type information for the terms?

>         3. Regarless, what other difficult implementation problems
> could be made to go away if the compiler directly support certain
> features? Semantics?

A related bothersome technical issue would be lambda term representation
and handling (in particular, conversions).

Best regards,
        David

THAT's   _\\/,  For a more realistic picture, my address and other stuff
NOT me:  (@ @)  see http://www.in.tum.de/~oheimb/                    ;<><
...---oOO-(_)-OOo-------------------------------------------------------