Difference between revisions of "Denotative design (Conal Elliott)"
(added related section and Conal Elliott) |
(→Related) |
||
| (3 intermediate revisions by the same user not shown) | |||
| Line 10: | Line 10: | ||
★ We need to start using computers to do these proofs automatedly. <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> | 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> | + | 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> | ★ Composing software without proof is like composing math or physics hypotheses without proof. <br> | ||
It goes exponentially downhill into delusion and self-deception. <br> | It goes exponentially downhill into delusion and self-deception. <br> | ||
| Line 17: | Line 17: | ||
Thus specifications absolutely need to be understandable and "elegant". <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> | '''"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> | + | <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> | 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> | ★ Specifications for desired properties for operational semantics are too inherently complex to be "elegant". <br> | ||
| Line 33: | Line 35: | ||
* [[Software]] | * [[Software]] | ||
* '''[[New software crisis]]''' | * '''[[New software crisis]]''' | ||
| + | * [[Denotative design (Conal Elliott)|Denotative design]] applied to and combined with [[Compiling to categories (Conal Elliott)|compiling to categories]] <br>gives a way to implement complex software correctly on various high performance [[compute architectures]] | ||
[[Category:Conal_Elliott|Conal Elliott]] | [[Category:Conal_Elliott|Conal Elliott]] | ||
Latest revision as of 10:14, 5 September 2024
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.
Note that beside the implementation the proof too does not need to be "elegant".
Only the specification (the starting point for the proof) needs to be "elegant".
★ 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)
Related
- Software
- New software crisis
- Denotative design applied to and combined with compiling to categories
gives a way to implement complex software correctly on various high performance compute architectures
