[Haskell-cafe] ghci start-up banner

[Cetin Sert]

Hi all,

after reading this announcement on the Galois blog:

http://www.galois.com/blog/2008/11/13/tech-talk-mechanically-verified-lisp-interpreters/

I installed Hol4 to play around with it a little bit.

I made 2 obvious observations ^_^:

1) It looks like the Hol4 system is just a ML module that gets loaded into
the Moscow ML interpreter with the help of a script
2) it prints a custom banner after loading

And now I have the following questions:

== about proof assistants in general ==
1) how many other proof assistants are built the same way as Hol4: as a
module loaded into some interpreter?
2) is there a paper or even better a funny but detailed comparison of proof
assistants?

== about custom banners at module load time ==
1) is there a way to do it in ghci?

Regards,
CS
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20081114/f95bd557/attachment.htm