Hi all,<br><br>after reading this announcement on the Galois blog:<br><br><div style="margin-left: 40px;"><a href="http://www.galois.com/blog/2008/11/13/tech-talk-mechanically-verified-lisp-interpreters/">http://www.galois.com/blog/2008/11/13/tech-talk-mechanically-verified-lisp-interpreters/</a><br>
</div><br>I installed Hol4 to play around with it a little bit.<br><br>I made 2 obvious observations ^_^:<br><br>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<br>
2) it prints a custom banner after loading<br><br>And now I have the following questions:<br><br>== about proof assistants in general ==<br>1) how many other proof assistants are built the same way as Hol4: as a module loaded into some interpreter?<br>
2) is there a paper or even better a funny but detailed comparison of proof assistants?<br><br>== about custom banners at module load time ==<br>1) is there a way to do it in ghci?<br><br>Regards,<br>CS<br>