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

On 6/16/06, Matthias Felleisen <matthias at ccs.neu.edu> wrote:
> You type check ONCE not every time you launch the program. Similarly,
> you prove things about the program ONCE, not every time you launch the
> program. However, while you are developing the program, launching (via
> RUN) and proving always coincides. Hence it is an issue to be solved
> within the program development environment not the compiler. --
> Matthias

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.

-- 
Carl Eastlund
"Cynical, but technically correct."