[plt-scheme] Schemebelle?

On Mon, Apr 27, 2009 at 9:53 PM, Carl Eastlund <carl.eastlund at gmail.com> wrote:
> On Mon, Apr 27, 2009 at 5:27 PM, Paulo J. Matos <pocmatos at gmail.com> wrote:
>>
>>> As someone familiar with Scheme and ACL2 (and to a lesser extent Typed
>>> Scheme and other theorem provers like Isabelle), I think there are
>>> tradeoffs to either approach.
>>>
>>> Any theorem prover you use will force you to reason about a pure
>>> subset of the language; you can generally only reason about mutation
>>> and other side effects by explicit state-passing (with a monad or
>>> something similar).
>>>
>>
>> From your considerations I assume then that by using an explicit
>> state-passing method you can make your impure program, pure. This is
>> after all, what Haskell does with monads. So you can 'indirectly'
>> reason about impure programs, right?
>
> That is correct, and there are plenty of examples of this being done
> with various theorem provers.  However, this kind of indirection can
> come with a high price in terms of complexity of verification.  In
> general, mechanical verification is significantly trickier than
> program development; you need the simplest possible representation of
> your program if you're going to verify it with a reasonable amount of
> effort.  You're always better off if you can model your program
> directly, and with current theorem proving technology that means
> finding a pure (non-store-passing) solution if at all possible.
>

OK!

>>> ACL2 reasons about pure, first-order Common Lisp, which is inches away
>>> from being pure, first-order Scheme.  If you want to reason about
>>> Scheme with ACL2, it shouldn't be too hard (to adapt the theorem
>>> prover to Scheme, or port your code to Lisp), IF you are willing to
>>> give up higher-order functions.  That's a big if (though ACL2's
>>> Lisp-style macros do help express some higher-order idioms in a
>>> first-order world).
>>
>> Regarding higher-order. I have to use first order because ACL2 is
>> automated [the proving] and doesn't allow higher order functions,
>> right?. On the other hand Isabelle uses Higher Order logic (but is
>> interactive) so I could in theory easily do proving with higher order
>> functions. I guess Haskabelle doesn't restrict the user to 1st
>> order... [know that my knowledge of theorem proving is limited so
>> nothing I say here should be considered certain, let me know if I
>> missed anything]
>
> I'm not sure that automated vs. interactive is really relevant here.
> ACL2 is first-order and HOL higher-order because those are the kinds
> of logics they were designed for.  I don't know of any reason one
> couldn't develop ACL2-style automation for HOL, for instance.  And
> ACL2, though "automatic" in some respects, does require user
> intervention for proofs of any significant complexity.  "Automatic"
> and "interactive" are not mutually exclusive.
>

Got it, that's true. My assumption, was that generally HOL ->
interactive proving and FOL -> automated. But obviously there is a
grey area since there might be times where automated provers may not
be fully automated requiring intervention from the user (called
mechanical, I think) and interactive might have automated parts
(recall auto tactics and the sledgehammer part of isabelle). Anyway, I
guess I was just confusing in my sentences and I apologise.

However, this comes in interesting times. I have been studying the
implementation of efficient model checkers for a specific formal
language in my PhD. I am doing this in Scheme so I have the models
represented as an AST  in Scheme. It is straightforward to dump a
scheme/lisp program that 'executes' this specification. How hard is it
to integrate it with dracula, I mean, run dracula automatically and
interact with it? I guess I could integrate it with ACL2 [unless
dracula adds features to ACL2, does it?] but since dracula is scheme
already, sending models to acl2, and interacting with it for proofs
requiring user intervention might be easier if I reuse parts of
dracula code, right?

This would allow me 'as a bonus' to perform theorem proving on models
besides model checking.

Cheers,

Paulo Matos

> --
> Carl Eastlund
>



-- 
Paulo Jorge Matos - pocmatos at gmail.com
Webpage: http://www.personal.soton.ac.uk/pocm