SoG Goal
SoG functions through establishing a fair and just political process in a world overwhelmed by the asymmetric distribution of data governance technologies. It provides a trustworthy foundation to help governing bodies allocate resources to execute policies efficiently, utilizing different aspects of established governance theories and creating new governance theories, while employing readily available technologies to deploy solutions in the real world. In other words, an End-to-End solution for governance must have a scientific basis that can be scaled up in applications through technology and have a unifying policy decision frame that can be applied to all application domains. This requires the Science of Governance to be abstract, so that it does not associate itself with a specific application context. It also needs to be concrete, so that all policy decisions are observable and accountable in terms of socially and physically meaningful data. The only medium to deal with this dualism is nothing but logic, more precisely, the logic of Correct by Design (CbD).
The Science of Policy Correctness
Before CbD is explained, one must understand the term “correctness.” There is a logical way to express correctness that is scale-free and domain-independent: the Venn Diagram representation of correctness in the diagram on the next page. It shows that correctness is the logical intersection of safety and liveness conditions. From a scientific viewpoint, correctness should be objectively determined according to explicitly encoded safety and liveness “social contracts”.
Safety means nothing bad happens: a system or policy is considered safe if nothing bad happens from its execution. If one plays a football game, and throughout the game, the player is not injured, the game is considered to be safe.
Liveness means something good happens during the execution of a system or policy. An example of this in a football game would be the player scoring a goal. That would be a liveness condition. The intersection between safety and liveness is clear in this example, a person is uninjured and scores a goal in the game. This is “correctness.”
This generic, domain-independent statement of correctness is not only applicable to computer science, but to governments as well. It allows policy designers to separately list the conditions of what are considered to be bad, and then list the conditions that are considered to be good. This logical decomposition of correctness is a powerful intellectual construct that enabled system engineers and computer scientists to build systems as complex as the Internet. Whether a governing body can consistently apply this construct in policy framing decides how well an organization may be governed by explicit rules. With an increasing amount of conditions, however, organizations need an additional way to ensure correctness, particularly in contracts. This is where Hoare Logic, Hoare triplets, and CbD comes in.
In 1969, when more possible conditions were being created in computer programming, Tony Hoare created a logic system to rigorously clarify system correctness. Key to this system was the Hoare Triple, expressed as {P} C {Q}. {P} is the precondition, what caused the command. C is the command, the action that takes place. {Q} is the postcondition, what happened due to the command’s occurrence. In terms of System Correctness, safety would be the precondition, the event occurring due to satisfying safeness would be the command, and liveness would be the postcondition. When C satisfied both {P} and {Q}, the system worked as planned, as in, it was Correct by Design.
In our football game example, {P} would be a person who is physically fit to play and that person does not have an intention/history to hurt other players. C would be playing the game, and {Q} would be the player scoring goals and playing at least 90 minutes. We know this example is Correct by Design if these parameters occurred accordingly. But if {Q} was the game only being played for 10 minutes and fog stopping the game, then we know the system did not attain correctness in terms of Correct by Design! CbD provides logical symmetry to all systems of any kind by using a consistent set of rules to classify the safety and liveness conditions of the system. This naming convention allows any system to identify errors (safety) and recognize accomplishment (liveness). As Henry Poicare once said: ”Mathematics is the art of giving the same name to different things.” CbD assigns consistent naming schemes (safety, liveness, and correctness) to all governance structures in casual categories.
Hoare Triples can go beyond computer programming, however, because every action made by every individual, group, government, etc. can be turned into a Hoare Triple. This includes something as simple as eating food. “Hunger” would be the pre-condition, “eating digestible food” would be the command, and “increased energy” would be the post-condition. Governance concepts like Rousseau’s Social Contract can be turned into a triplet as well. People giving power to a government would be the pre-condition, the creation of a Social Contract would be the Command, while the government receiving power would be the post-condition. These triplets can be simple or detailed, and one can even form a chain of triplets using the post-condition as the new pre-condition for a new triplet. One can easily imagine these Hoare Triples to be linked/composed to express more complex policies or programs. It is the complexity of these composable arrows/Hoare Triples that make it a domain-independent way to organize correctness in a formalized data structure. This logic system is instrumental in guiding people in a world of increasingly complex contracts.
Writing down satisfactory conditions in contracts is not new. What is new are the many possible conditions in this already highly interconnected world. Yet all these possibilities can be symmetrically dealt with through Hoare logic and concepts that formally frame correctness like CbD. Due to its composability, Hoare Triples may serve as the universal data primitive to encode arbitrary large-scale social and industrial governance challenges. Due to its simplicity, they can scaffold application scenarios that deal with the complex interactions of many knowledge domains. The Hoare Triple is a Universal Construct: It is everywhere and has been already adopted by many popular governance tools, such as the Logic Model (see Appendix on Logic Model as Multi-Level Hoare Triples).