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
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
