Denotative design (Conal Elliott)
High level philosophy
★ Reliability of SW is always exponentially dropping with successive composition.
SW with formal specification and formal proof of desired behavior is the one single exception. …
★ Several things are limited by this exponential drop of scalability of reliability:
— essential irreducible complexity of our SW
— performance of our SW as it requires optimization which critically depends on higher essential complexity …
★ We need to start using computers to do these proofs automatedly.
That is: Start using (and making) practical proglangs that can proof (denotatively) specified desired behaviors about their programs.
This is what dependent typing provides. Thus we need dependent typing. …
★ Composing software without proof is like composing math or physics hypotheses without proof.
It goes exponentially downhill into delusion and self-deception.
Thus Conal Elliott claims we are still in the pre-scientific dark ages of computing. …
★ Not understanding the specification of a desired property makes its proof useless.
Thus specifications absolutely need to be understandable and "elegant".
"Elegant" in the sense of being tersely describable by math learned for other good practical reasons.
★ Having the imperative (operational semantics) paradigm at the very core of a language is embodying non-physical single threadedness (the von Neumann bottleneck).
This is so bad that it makes even the best specifications about desired properties incomprehensible. That is: …
★ Specifications for desired properties for operational semantics are too inherently complex to be "elegant".
Thus they defeat their purpose.
★ We need languages with denotational semantics (what is true) rather than operational semantics (what to do in sequence) at their core
in order to have elegant specifications of desired program properties and thus scaleable reliability
and as collary: scaleable comprehensibility, and scaleable performance
Concrete approach
(wiki-TODO: Make a summary here)
