&gt;Of course, we need to reach a gentleman&#x27;s agreement regarding which formalism is a good “foundation” for defining everything else. My personal preference would be to define all other formal systems in terms of rules of inference.<p>If you are interested in defining &quot;low cognitive load&quot; that&#x27;s a poor choice, in my opinion.<p>&gt;I am fine with any, as long as the same choice is made for all languages being compared. What ultimately interests me is proving a type safety theorem, that is, a precise sense in which “well typed programs don&#x27;t go wrong”, so perhaps this makes a structural operational semantics more appropriate than the other choices.<p>I&#x27;m not aware of any such thing, the kinds of formal semantics that academics prefer deal very poorly with the realities of finite execution speed and memory, the kinds that pratictioners use (which usually isn&#x27;t referred to as &quot;formal semantics&quot; but rather &quot;what does this compile to&quot;) deal very poorly output correctness.<p>However this has little to do with cognitive load, even if such formal semantics existed it doesn&#x27;t necessarily mean it would be easy for a human mind.<p>&gt; Sure, but the target languages used by most compilers are often themselves very complex. Which means a realistic compiler or interpreter most likely won&#x27;t be a good benchmark for semantic simplicity.<p>If you agree that formal semantics is just a translation from one formalism to another, you can&#x27;t claim that a formalism A is semantically more complex than formalism B without picking a formalism C as a reference point.