Home

ACL2 in DrScheme

Via the plt-scheme mailing list:

We are pleased to announce the first public release [beta 7] of ACL2
in DrScheme, a combination of the ACL2 theorem prover system with the
DrScheme programming environment. The objective of this project is
to provide a development environment for ACL2 suitable for novice
users as well as enhancements of ACL2 that are attractive for the
typical undergraduate student (graphics, interactive games, sound).

There's a tutorial with screenshots and some examples on the ACL2 in DrScheme web page.

I'm always happy to see reasoning about programs introduced at the undergraduate level. I wonder what the LtU community would do with a tool like this. What cool things would you teach with a beginner's theorem prover?

By Dave Herman at 2006-03-08 14:21 | Functional | Logic/Declarative | Teaching & Learning | other blogs | 15740 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

What I'd teach undergrads with ACL2

Patience.

By ChasRMartin at Wed, 2006-03-08 16:45 | login or register to post comments

Wait, whoa.

Firstly, I think my mind got blown. Secondly, I have some important questions that I'm having trouble answering via the online docs.

1. Most importantly: is this a native Scheme implementation of ACL2, or is it a user interface for ACL2 built using the PLT tools?
2. If it is not a native implementation, is it a graphical interface, or does it use MzScheme FFI so that Scheme code and ACL2 code can be mixed?

By David Fisher at Wed, 2006-03-08 17:52 | login or register to post comments

not native Scheme

It seems the PLT people have built some version of CommonLisp for DrScheme. You can define & execute fns in this language, without even installing ACL2 (which e.g. I can't right now, since I'm in MSWindows).

To get proofs, though, you have to have ACL2 installed.

I couldn't find any documentation on what exactly their CL-like language is - it looks like it might be the same as ACL2's.

As I understand things, DrScheme supports languages via the MzScheme module system, so you can mix things freely after importing them.
For ACL2 to reason about them, you (AFAICT) have to extend ACL2's knowledge via declarations. Maybe that will be enhanced, though.

They have examples where ACL2 "reasons about" some GUI fns provided by DrScheme.
I always thought worms could be subdivided, but they prove otherwise!

By dbfaken at Wed, 2006-03-08 22:20 | login or register to post comments

Oh my. That would be the

Oh my. That would be the best possible scenario.

The MzScheme language extension facility is the same as in any Scheme implementation -- through hygenic macros. The details of low-level macros are certainly implementation-dependent, but the high-level macros are R5RS compliant, for what that's worth. If they have implemented CL as Scheme macros, that would, in fact, make it a native implementation of CL in Scheme, quite an accomplishment.

ACL2 is inextricably bound to its host language. While the language itself is a subset of CL (a very small subset, indeed -- for example, functions must terminate!), there are ways to escape to the host language, for example, in macros.

By David Fisher at Thu, 2006-03-09 00:23 | login or register to post comments

More or less, yes

I couldn't find any documentation on what exactly their CL-like language is - it looks like it might be the same as ACL2's.

This is correct. ACL2 is both a programming language (Applicative Common Lisp) and a theorem prover for that language (A Computational Logic). Our tool implements (a portion of) the former.

For ACL2 to reason about them, you (AFAICT) have to extend ACL2's knowledge via declarations.

Right again. We provide such declarations for the additional functionality that we support, but you can also write your own if you already know ACL2.

... without even installing ACL2 (which e.g. I can't right now, since I'm in MSWindows).

Actually, Jared Davis has built a Windows installer. It includes GCL and Emacs too.

I always thought worms could be subdivided, but they prove otherwise!
We stand against such destructive updates ;)

By dalev at Fri, 2006-03-10 03:51 | login or register to post comments

ACL2 '06

There's a forthcoming workshop on ACL2 in Seattle this coming August (it's one of the hundreds of FLoC satellites, my these academic gatherings are getting huge). There's a call for papers out, and the PC looks strong, but I don't see any invited speakers, and there is noone I recognise to be a scheme hacker on the PC.

By Charles Stewart at Wed, 2006-03-22 20:22 | login or register to post comments

discrete math

Simple proof homeworks in discrete math classes will be more well-received.

A frustration over proof homework is students aren't sure what is invalid; they have to wait two weeks for the grading. They also get the impression that the metric is subjective due to excessive use of natural language.

With something like ACL2 they get immediate feedback. They also get an assurance of objectivity.

By Albert Y.C. Lai at Sat, 2006-04-01 01:57 | login or register to post comments