Hi all,
after reading this announcement on the Galois blog:
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