[plt-scheme] Schemebelle?

On Mon, Apr 27, 2009 at 6:58 PM, Carl Eastlund <carl.eastlund at gmail.com> wrote:
> On Mon, Apr 27, 2009 at 1:30 PM, Sam TH <samth at ccs.neu.edu> wrote:
>> On Mon, Apr 27, 2009 at 1:19 PM, Paulo J. Matos <pocmatos at gmail.com> wrote:
>>>
>>> Now, I am wondering, how hard would it be to get something done for
>>> Scheme (and is there any interest from the community)?
>>> I would guess one major issue would be typing, but I would guess
>>> typed-scheme would makes things easier for a possible schemebelle?
>>
>> I doubt it.  Typed Scheme has a (very) different type system from
>> Isabelle, and Haskell and Isabelle are both pure languages, whereas
>> Scheme is not.
>>
>> If you want to go the "translate Scheme into a theorem prover" route,
>> ACL2 might be a better option.
>

First of all, thanks for your extended reply.

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

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

> On the other hand, Isabelle reasons about pure, typed... I don't know
> what the language is called.  But I speculate that if you want to
> reason about Scheme with Isabelle/HOL, it shouldn't be too hard, IF
> you are wiling to bridge the gap between typed and untyped idioms
> (either by translating your Scheme code to use Isabelle pattern
> matching and typed idioms, or representing the set of Scheme values as
> a big Isabelle datatype).  That's another big if.
>

I see...

> Scheme is kind of caught in the middle of these two kinds of
> languages.  There is currently no Scheme-based theorem prover I know
> if.  If you want to apply automated theorem proving to Scheme code you
> have to translate away either your higher-order functions or your
> untyped idioms, or you have to write a new theorem prover.
>

I get the problem... :)

> My thesis topic relates to some of this stuff -- I am working on
> extensions to the language of ACL2.  For instance, Modular ACL2 [1]
> (distributed with Dracula) allows a restricted form of higher-order
> reasoning; however, it's all static, you don't get to pass functions
> around at runtime.  I've also done some work on reasoning about impure
> and non-terminating programs (specifically, the "world teachpack" from
> DrScheme [2]).  And of course I am building on prior work for all of
> these ideas (ACL2's encapsulation and functional instantiation for
> abstract reasoning [3], single-threaded objects for reasoning about
> I/O [4], and methods for modelling potentially non-terminating state
> machines [5] and tail-recursive functions [6]).  But I don't know of
> any general solution for verifying impure, partial, or higher order
> functions in ACL2; at some point these represent fundamental
> limitations of the theorem prover.
>

Great, thanks for letting me know about this and about all the references!!! :D

> --
> Carl Eastlund
>
> [1] Eastlund, C. and M. Felleisen.  Toward a Practical Module System
> for ACL2.  In Proceedings of the 11th International Symposium on
> Practical Aspects of Declarative Languages, p. 46-60.  Springer, 2009.
>
> [2] Eastlund, C. and M. Felleisen.  Automatic Verification of
> Interactive Graphical Programs.  In Proceedings of the 8th
> International Workshop on the ACL2 Theorem Prover and its
> Applications.  ACM Press, 2009; to appear.
>
> [3] Kaufmann, M. and J S. Moore.  Structured Theory Development for a
> Mechanized Logic.  Journal of Automated Reasoning, 26(2):161-203,
> 2001.
>
> [4] Davis, J.  Reasoning about ACL2 File Input.  In Proceedings of the
> 6th International Workshop on the ACL2 Theorem Prover and its
> Applications, p. 117-126.  ACM Press, 2006.
>
> [5] Boyer, R. S. and J S. Moore.  Mechanized Formal Reasoning About
> Programs and Computing Machines.  In "Automated Reasoning and its
> Applications: Essays in Honor of Larry Wos," p. 146-176.  MIT Press,
> 1996.
>
> [6] Manolios, P. and J S. Moore.  Partial Functions in ACL2.  Journal
> of Automated Reasoning, 31(2):107-127, 2003.
>



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