Re: [Hol-info] What is the advantage of HOL4?

Some strengths of HOL4 (off the top of my head, so maybe not comprehensive): - It is based on simple type theory. See "The seven virtues of simple type theory" . - It is implemented in Standard ML. This is a formally specifi

[Hol-info] What is the advantage of HOL4?

Hi,guys I am working with HOL4. Recently, I read some papers, knowing that there are some other theorem provers, like PVS,COQ. They are similar in many aspects. For example, the logic used by them is Higher order logic. I am wondering What is the advantage of HOL4? Thanks!---