View source for Denotative design (Conal Elliott)

{{stub}}

== High level philosophy ==

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

== Concrete approach ==

{{wikitodo|Make a summary here}}