[plt-scheme] Schemebelle?

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