🚀 go-pugleaf

Someone in this newsgroup a while ago mentioned LCF.
I am wondering if anyone out there has any experience with this
system that they could let me know about. We have a copy of
a Franz Lisp version from Goteburg that runs on the VAX,
but not much has been done with it here. I find it quite interesting
except that I am upset by a fairly glaring problem in its logic, viz:
the inability to add predictates. You can add other constants,
but they are all function symbols. This means that you cannot
use logical formulas with NOT, OR, IFF, amongst others, in them.
You can define these things after a fashion, but they remain terms,
and cant be readily manipulated. Does anybody know anything about this
problem?

In general, I am interested in systems that could be considered
"aids to the working mathematician", in the sense of convenient
and helpful interaction, proof checking, and the ability to program
sophisticated proof strategies. LCF wins as a first start in some
ways, but in other ways it is dismal.
It wins because of the language ML that allows that programming
of proof techniques; this is lacking in the other systems I know of.
However, it seems to require an awful lot of detail, and its logic
is not too flexible, especially in terms of subsuming detail. Also,
it proof management schemes are vastly inferior to Affirm's, it seems.

Other systems I know a little about include Affirm (Gerhart, et al)
Automath (de Bruijn), FOL (Weyrauch).
I would like to hear from anybody interested in or doing work
(developing or using) such systems.

If anyone thinks this is sort of out of place material for this newgroup
(which unfortunately seems to be dead), I would be glad to explain why I
believe that it most certainly is not.