[plt-scheme] Schemebelle?

On Mon, Apr 27, 2009 at 5: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.
>

Yes, I agree... I guess having dracula integrated with plt-scheme
helps but I was more wondering what would the research challenges one
would face?

I am research-wise more familiar with model checking than with theorem
proving so this might well be out of my league here but I was just
curious if anyone knows about this.

Cheers,

Paulo Matos

> --
> sam th
> samth at ccs.neu.edu
>



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