[plt-scheme] on-execute method in drscheme:language:language<%>

I thought I was contradicting you.  What I spelled out is entirely
consistent with doing theorem proving or type checking at syntax
expansion time.

On 6/16/06, Matthias Felleisen <matthias at ccs.neu.edu> wrote:
> Thanks for spelling out the details. I was hoping Eli would know those.
> -- Matthias
>
> On Jun 16, 2006, at 12:31 PM, Carl Eastlund wrote:
> >
> > You type check every time you start with a program that might not have
> > been checked yet.  In compiled languages, this is easy to keep track
> > of: once it's compiled, you're set.  Similarly with MzScheme, once
> > something in Dale's theorem-prover-based language is a .zo, he
> > probably doesn't need to check it again.  But if it runs again from
> > source, unless you annotate and save the theorem with the source code,
> > how can you avoid running the theorem prover again?  It seems to me
> > you're going to have to prove theorems approximately as often as you
> > expand syntax, one way or another.