Take a look at Dracula, the ACL2 support from DrScheme. It implements exactly that behavior. (You may even wish to take a look at our How to prove curriculum addition to HtDP. We teach freshmen how to prove theorems about graphical games.)
Two points about it: 1. in the presence of true effects (not counting infinite loops), this model doesn't really work 2. and it is not a mid-point between the two extremes but a new, third point. What my blog post omits is a research attempt to explore a true midpoint between the two. Before we started the drscheme project in 1995, I worked with Rene Rodriguez and Bruce Duba on a transparent REPL for Emacs. We implemented it and used it with our freshman course for at least two semesters. Here is how it worked: use an ordinary emacs interaction mode control emacs interactions via a dependency analysis if sending an s-expression were to violate a dependency, re-load the entire buffer (or a lot of it) for I/O, we had a separate buffer that could differentiate between committed and preliminary output In the presence of HO and effectful computations, a dependency analysis is of course a conservative approximation. So this is highly approximate but for introductory classes it worked reasonably well. We gave up on this effort because we didn't get this repl to work for experienced users, it didn't really cope well with effects, and the effort had to replicate a lot of the work of the underlying compiler (Chez Scheme) so we had no research benefit. The drscheme project gave us a chance to try an even more radical approach, and I think it has worked well for beginners. To be honest, on and off I do think about a way to accommodate a Lisp-style repl or some flavor of it, but it sure isn't a high priority. -- Matthias On Jun 24, 2010, at 9:11 AM, Nadeem Abdul Hamid wrote: >> See >> http://blog.racket-lang.org/2009/03/drscheme-repl-isnt-lisp.html >> for a detailed answer. >> > > I see what the blog post above is saying, but (I know, "no when no if no > but"), has anyone ever used editors for some of the proof assistants, like > CoqIDE or ProofGeneral mode in Emacs for Coq? These support a seemingly nice > compromise between the two styles. A minor annoyance I have with the DrRacket > model of reloading the entire buffer is that if I have several working > functions defined at the top of the file, and then a new function I'm working > on below that has syntax errors or is in incomplete template form or > whatever, running the file generates an error and no definitions at all are > loaded into the REPL. So instead, in these proof editors, they have this > feature where you can load the buffer up to a certain line/expression > (assuming no syntax errors), and everything above there is then in a "locked" > (uneditable) mode -- if you edit something, it rolls back the evaluated > portion of the file. This way, you can have a bunch of messy/incomplete > thoughts typed up at the ! bo! > ttom of your file, and have all good definitions up to a certain point in > your file evaluated so that you can play with the evaluated definitions in > the REPL, to help you fill in your unfinished thoughts. I know, this will get > messy in the presence of effects (proof languages are purely functional), and > probably a lot of work to implement, but something to think about... > > > --- nadeem > > _________________________________________________ > For list-related administrative tasks: > http://lists.racket-lang.org/listinfo/users _________________________________________________ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/users
