There is also a misunderstanding of terminology outside the LCF community. In some quarters today the decomposition to primitives is supposed to be the distinguishing feature of a 'tactic'. Some writers use this notion for a Hilbert-style proof system. In that case the definitions are slightly different. 44 Note that the formalized provability is for the original system, without the reflection rule.
Care is needed if instances of the reflection rule are to be nested.
By Tarski's theorem we can't actually have a predicate representing truth, but the above axioms say something intuitively close. 46 One may say that the ML programming language is the metalogic of LCF systems, but a peculiarly limited or ultra-constructive one where the only way of proving something exists is to produce it explicitly. The author has been told that an attempt was made to verify in Nuprl the correctness of a Presburger arithmetic implementation, but the researcher involved eventually became discouraged by the difficulty of the proofs. It has been remarked that computer scientists would rather use each other's toothbrushes than each other's notation. Unfortunately, the fact that the few informal parts of his formalized mathematics was written in latino sine flexione must have contributed to their limited impact.