[plt-scheme] Schemebelle?

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.

-- 
sam th
samth at ccs.neu.edu