[plt-scheme] Schemebelle?

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.

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

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

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.

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.

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.

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