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

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


On Jun 16, 2006, at 11:57 AM, Eli Barzilay wrote:

> On Jun 16, Matthias Felleisen wrote:
>> I think that's precisely what you don't want.
>
> ??
>
>> This is an environmental issue not a programming issue. Suppose you
>> are creating an executable.  All you want for this thing is to run;
>> you don't want it to prove theorems, interactively, after you have
>> carefully proven this program correct.
>
> Sounds like it precisely what I *do* want!  To create an executable I
> have to compile the file in advance -- the compilation process expands
> macros, which forces me to prove the code correct.  The existence of
> the compiled code becomes the certificate that the relevant proofs
> were done.  Just like type-checking.
>
>
>> On Jun 16, 2006, at 11:49 AM, Eli Barzilay wrote:
>>
>>> On Jun 16, Dale Vaillancourt wrote:
>>>> I need to "type-check" a program before running.  If it doesn't
>>>> pass, I want to reject the attempt to run.  The checking is done by
>>>> submitting the text in the definitions window to an external theorem
>>>> prover.
>>>>
>>>> You are right about execute-callback not being quite what I want,
>>>> btw.  That captures all clicks on `Run', even when my language is
>>>> not the one associated with the current tab.
>>>
>>> Wouldn't that be better to do at syntax-expansion time?  Something
>>> like overriding #%module-begin for module code, and the evaluation
>>> handler for other toplevel interactions?  (And that will make it
>>> possible to use outside of DrScheme.)
>>>
>>> -- 
>>>           ((lambda (x) (x x)) (lambda (x) (x x)))          Eli
>>> Barzilay:
>>>                   http://www.barzilay.org/                 Maze is
>>> Life!
>>> _________________________________________________
>>>   For list-related administrative tasks:
>>>   http://list.cs.brown.edu/mailman/listinfo/plt-scheme
>>
>
> -- 
>           ((lambda (x) (x x)) (lambda (x) (x x)))          Eli 
> Barzilay:
>                   http://www.barzilay.org/                 Maze is 
> Life!
> _________________________________________________
>   For list-related administrative tasks:
>   http://list.cs.brown.edu/mailman/listinfo/plt-scheme