Mathematical models only prove consistency relative to classical set theory (or whatever other meta-theory we are using). Is it possible to be convinced about the consistency of the theory in a more direct way, so called simple minded consistency (Martin-Löf 1984)? In fact, is there a way to explain what it means for a judgment to be correct in a direct pre-mathematical way? And given that we know what the judgments mean can we then be convinced that the inference rules of the theory are valid? An answer to this problem was proposed by Martin-Löf in 1979 in the paper “Constructive Mathematics and Computer Programming” (Martin-Löf 1982) and elaborated later on in numerous lectures and notes, see for example, Martin-Löf (1984, 1987). These meaning explanations for intuitionistic type theory are also referred to as the direct semantics, intuitive semantics, informal semantics, standard semantics, or the syntactico-semantical approach to meaning theory.