[plt-scheme] Schemebelle?

From: Carl Eastlund (carl.eastlund at gmail.com)
Date: Mon Apr 27 17:53:52 EDT 2009

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.

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

Carl Eastlund

Posted on the users mailing list.