  The Logic of Proofs  \(\mathsf{LP}\)  became the first in the Justification Logic  family. Proof terms in  \(\mathsf{LP}\)  are nothing but BHK terms understood as  classical proofs. With  \(\mathsf{LP}\),  propositional intuitionistic logic received  the desired rigorous BHK semantics: