4 ms·
>Of course, we need to reach a gentleman's agreement regarding which formalism is a good “foundation” for defining everything else. My personal preference would
by EdiX 11y ago
>Of course, we need to reach a gentleman'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.
If you are interested in defining "low cognitive load" that's a poor choice, in my opinion.
>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't go wrong”, so perhaps this makes a structural operational semantics more appropriate than the other choices.
I'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't referred to as "formal semantics" but rather "what does this compile to") deal very poorly output correctness.
However this has little to do with cognitive load, even if such formal semantics existed it doesn't necessarily mean it would be easy for a human mind.
> Sure, but the target languages used by most compilers are often themselves very complex. Which means a realistic compiler or interpreter most likely won't be a good benchmark for semantic simplicity.
If you agree that formal semantics is just a translation from one formalism to another, you can't claim that a formalism A is semantically more complex than formalism B without picking a formalism C as a reference point.
- catnaroek 11y ago> If you are interested in defining "low cognitive load" that's a poor choice, in my opinion. I'm interested in “low cognitive load without sacrificing technical precision.” It's a much harder goal to achieve than “low cognitive load if we hand-wave the tricky details.” > However this has little to do with cognitive load, even if such formal semantics existed it doesn't necessarily mean it would be easy for a human mind. Which is exactly my point. I only consider a language simple if its formal description is simple. > If you agree that formal semantics is just a translation from one formalism to another, you can't claim that a formalism A is semantically more complex than formalism B without picking a formalism C as a reference point. No disagreement here. I even stated my personal choice of C.
- EdiX 11y ago> I'm interested in “low cognitive load without sacrificing technical precision.” You don't seem to be interested in low cognitive load at all, otherwise: > No disagreement here. I even stated my personal choice of C. you would have attempted to motivated your choice of reference point in terms of cognitive load. Even if induction mathematics was the way the human mind worked (which it isn't) it's very different from CPUs and there is a cognitive load (and semantical distance) in going from mathematics to CPUs.
- catnaroek 11y ago> Even if induction mathematics was the way the human mind worked (which it isn't) Even if it isn't how the human mind works, it's how computing itself works. Would you take seriously a physicist who denies gravity? I wouldn't take seriously a computer scientist who denies structural induction.
- EdiX 11y ago> it's how computing itself works but it's not the whole story when it comes to computers.