[plt-scheme] Schemebelle?

Hi all,

One the topics I am involved in my PhD and interested also in my past
time is formal software verification.
I just noticed that the Isabelle people released Haskelbelle
(http://www.cl.cam.ac.uk/research/hvg/Isabelle/haskabelle.html)
"Haskabelle is a converter from Haskell source files to Isabelle/HOL
theories implemented in Haskell itself."

A simple introduction is found in this blog post:
http://www.jedi-ninja.net/2009/04/20/A-little-fun.html

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?

Any comments/references to research are welcome.

Cheers,


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