[plt-scheme] on-execute method in drscheme:language:language<%>
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:
> 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."