Denotative design (Conal Elliott) - Revision history

Apm: /* Related */

2024-09-05T09:14:35Z

← Older revision		Revision as of 11:14, 5 September 2024
Line 35:		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]]

Apm: link to yet unwritten page von Neumann bottleneck

2023-07-11T06:47:24Z

link to yet unwritten page von Neumann bottleneck

← Older revision		Revision as of 08:47, 11 July 2023
Line 19:		Line 19:
	<small>Note that beside the implementation the proof too does not need to be "elegant".</small> <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>		<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>		★ 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>

Apm: /* High level philosophy */ only specification needs to be "elegant" not the proof

2023-07-11T06:45:52Z

High level philosophy: only specification needs to be "elegant" not the proof

← Older revision		Revision as of 08:45, 11 July 2023
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>
			<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>		★ 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>

Apm: /* High level philosophy */

2023-07-11T06:41:27Z

High level philosophy

← Older revision		Revision as of 08:41, 11 July 2023
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>

Apm: added related section and Conal Elliott

2023-07-11T06:40:11Z

added related section and Conal Elliott

← Older revision		Revision as of 08:40, 11 July 2023
Line 28:		Line 28:

	{{wikitodo\|Make a summary here}}		{{wikitodo\|Make a summary here}}

			== Related ==

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

			[[Category:Conal_Elliott\|Conal Elliott]]

Apm: basic page - still incomlete

2023-07-11T06:37:25Z

basic page - still incomlete

New page

{{stub}}

== 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 ==

{{wikitodo|Make a summary here}}