Difference between revisions of "Correct by design"
| (5 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
{{WikiEntry|key={{PAGENAME}}|qCode=}} is a design and engineering principle that all systems must be designed and built in ways that make incorrect implementation and usage is either infeasible or at least impractical. This maybe accomplished by thinking of everything in a unifying primitive, and making sure that all aspects of this primitive are systematically designed in ways that prevents error. One such approach is [[Anothony Hoare]]'s [[Hoare Triple]] or [[Hoare Logic]]. | {{WikiEntry|key={{PAGENAME}}|qCode=}} is a design and engineering principle that all systems must be designed and built in ways that make incorrect implementation and usage is either infeasible or at least impractical. This maybe accomplished by thinking of everything in a unifying primitive, and making sure that all aspects of this primitive are systematically designed in ways that prevents error. One such approach is [[Anothony Hoare]]'s [[Hoare Triple]] or [[Hoare Logic]]. Relevant efforts are [[Probably Approximately Correct]] by [[Leslie Valiant]] and [[Abstract Interpretation]] by [[Patrick Cousot]] and [[Rhadia Cousot]]. These theories and methodologies focus design and engineering efforts on [[correctness]] by considering [[soundness]]/[[completeness]], [[precision]], and [[terminability]] from the get go. | ||
There are some references on this subject: [https://eugenykolpakov.com/design/2021-07-24-correct-by-design/ Correct by Design] written by Eugeny Kolpakov. | <noinclude> | ||
From a pragmatic viewpoint, one may organize tools and technologies in ways to systematically track and avoid error, such as using [[Verion Control]], [[Blockchain]], [[User Interface]]/[[User Experience]], [[Ricardian Contract]], and [[Relational Database]] to capture the entirety of a system in ways that avoids mistakes. | |||
=Some Useful examples= | |||
#There are some references on this subject: [https://eugenykolpakov.com/design/2021-07-24-correct-by-design/ Correct by Design] written by Eugeny Kolpakov. | |||
#[https://www.undatarevolution.org/ United Nation's Data Revolution Website] | |||
#[https://rtg.cis.upenn.edu/hcmdss/Papers/submissions/35.pdf CORRECT-BY-DESIGN SOFTWARE IS FUNDAMENTAL TO HIGH-CONFIDENCE DEVICES] by S. J. Prowell. | |||
=Correctness in Data and Control Planes= | |||
To attain correctness in the world of cloud-computing, [[Data Plane]] is a kind of space that grounds the possibility space of system behavior. In contrast, [[Control Plane]] is a kind of space that mobilizes and reflects upon the state of the system of interest. The safety and liveness of Data and Control Planes make the system [[correct]]. | |||
{{PagePostfix | {{PagePostfix | ||
|category_csd=Hoare Logic | |category_csd=Hoare Logic,Correctness | ||
}} | }} | ||
</noinclude> | |||
Latest revision as of 05:14, 10 September 2022
Correct by design(Q) is a design and engineering principle that all systems must be designed and built in ways that make incorrect implementation and usage is either infeasible or at least impractical. This maybe accomplished by thinking of everything in a unifying primitive, and making sure that all aspects of this primitive are systematically designed in ways that prevents error. One such approach is Anothony Hoare's Hoare Triple or Hoare Logic. Relevant efforts are Probably Approximately Correct by Leslie Valiant and Abstract Interpretation by Patrick Cousot and Rhadia Cousot. These theories and methodologies focus design and engineering efforts on correctness by considering soundness/completeness, precision, and terminability from the get go.
From a pragmatic viewpoint, one may organize tools and technologies in ways to systematically track and avoid error, such as using Verion Control, Blockchain, User Interface/User Experience, Ricardian Contract, and Relational Database to capture the entirety of a system in ways that avoids mistakes.
Some Useful examples
- There are some references on this subject: Correct by Design written by Eugeny Kolpakov.
- United Nation's Data Revolution Website
- CORRECT-BY-DESIGN SOFTWARE IS FUNDAMENTAL TO HIGH-CONFIDENCE DEVICES by S. J. Prowell.
Correctness in Data and Control Planes
To attain correctness in the world of cloud-computing, Data Plane is a kind of space that grounds the possibility space of system behavior. In contrast, Control Plane is a kind of space that mobilizes and reflects upon the state of the system of interest. The safety and liveness of Data and Control Planes make the system correct.
References
Related Pages