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

From: Matthias Felleisen (matthias at ccs.neu.edu)
Date: Fri Jun 16 13:12:32 EDT 2006

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."



Posted on the users mailing list.