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>
<small>Note that beside the implementation the proof too does not need to be "elegant".</small> <br>
<small>Only the specification (the starting point for the proof) needs to be "elegant".</small> <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}}

== Related ==

* [[Software]]
* '''[[New software crisis]]'''

[[Category:Conal_Elliott|Conal Elliott]]