I never said the code enforces it. I said the formal specification can provide the most description clarity in terms of human communication of intention or rules. People know 1+1=2 not because I say it does, but because there is a formal proof which proves a+b=c and so on. These proofs are how we all agree that math is real, concrete, and that is why numbers and symbols have an absolute meaning.
My approach is to use the formal specification as the document which acts as the blockchain constitution or smart contract constitution. This is why I always was in favor of formal verification. What I do not want is an English document which can be interpreted any kind of way because natural language is horrible for determining meaning when compared to formal communications such as constrained or controlled natural language or formal specification.
The formal specification would make it so that every possible rule is formalized as mathematics. The Controlled English would make it so every English speaker could interpret the precise meaning without any ambiguity, doubt, or disagreement. 1+1=2 everywhere on the planet because of the formal proof behind the math. For the constitution, it should be as certain as 1+1=2 for each and every line and I can only think formal specification is the way to do it.
An interesting fact to note is you actually can encode the entire traditional legal system as mathematics. You can take the logic behind all forms of laws as well as contract types, and import it into software, and merge it. Legal ontologies exist such as LKIF.
In the formal specification you can always have dispute resolution capacity. This capacity could exist on a spectrum where the first resort is to resolve all disputes internally and only as the mechanisms fail should the final resort be to use off chain off cyberspace mechanisms which in my opinion should be included but should be the fallback mechanism of last resort.
a constitution could serve as a formal declaration of intentions for the code
We agree and that is what I was saying only what I'm saying is natural language isn't very formal. You can take a formal proof and every human on earth can interpret it exactly and precisely because it's the basis of math. On the other hand if you take natural language then you have so many different languages and within each language you have all sorts of dialects, buzzwords, and I want us to avoid the Tower of Babel effect we see elsewhere. Useful quote from Wolfram:
"So we’re slowly moving toward people being educated in the kind of computational paradigm. Which is good, because the way I see it, computation is going to become central to almost every field. Let's talk about two examples—classic professions: law and medicine. It's funny, when Leibniz was first thinking about computation at the end of the 1600s, the thing he wanted to do was to build a machine that would effectively answer legal questions. It was too early then. But now we’re almost ready, I think, for computational law. Where for example contracts become computational. They explicitly become algorithms that decide what's possible and what's not.You know, some pieces of this have already happened. Like with financial derivatives, like options and futures. In the past these used to just be natural language contracts. But then they got codified and parametrized. So they’re really just algorithms, which of course one can do meta-computations on, which is what has launched a thousand hedge funds, and so on. Well, eventually one's going to be able to make computational all sorts of legal things, from mortgages to tax codes to perhaps even patents. Now to actually achieve that, one has to have ways to represent many aspects of the real world, in all its messiness. Which is what the whole knowledge-based computing of Wolfram|Alpha is about."[29]
References
- https://en.wikipedia.org/wiki/Pythagorean_theorem
- https://en.wikipedia.org/wiki/Formal_proof
- https://en.wikipedia.org/wiki/Constructive_proof
- http://www.estrellaproject.org/lkif-core/
- https://github.com/RinkeHoekstra/lkif-core
- https://en.wikipedia.org/wiki/Tower_of_Babel
- https://sites.google.com/site/controllednaturallanguage/
- https://en.wikipedia.org/wiki/Computational_law
My background is not in mathematics, but it sounds to me that a proposed constitution written in a formal, mathematic language may be an idealistic impossibility.
Isn't this what Gödel proved impossible with his incompleteness theorem? Won't we inevitably have contradictions in any formal system of high enough complexity?