Could a formal spec act as a constitution for a blockchain?
I think you are missing the point. For me, the crucial role of a constitution is to cover areas which cannot be enforced by the code or achieved via economic incentives.
Apart from that, a constitution could serve as a formal declaration of intentions for the code, so that we can easily differentiate between bugs and features, but for me this is only a minor role, as the whitepaper does it quite effectively.
@dan , do I understand your approach correctly?
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.
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:
References
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?