Basic Model Theory and Input Validation
When speaking of Tauchain we must first have an understanding of Finite Model Theory.
Sometimes we write or speak a sentence S that expresses nothing either true or false, because some crucial information is missing about what the words mean. If we go on to add this information, so that S comes to express a true or false statement, we are said to interpret S, and the added information is called an interpretation of S. If the interpretation I happens to make S state something true, we say that I is a model of S, or that I satisfies S, in symbols ‘I ⊨ S’. Another way of saying that I is a model of S is to say that S is true in I, and so we have the notion of model-theoretic truth, which is truth in a particular interpretation. But one should remember that the statement ‘S is true in I’ is just a paraphrase of ‘S, when interpreted as in I, is true’; so model-theoretic truth is parasitic on plain ordinary truth, and we can always paraphrase it away.
The primary culprit the in security flaws to be found in future Ethereum smart contracts (malconstructed inputs)
In order to write secure software we must be aware of the rule that quality input is of primary importance to produce quality output. A well defined, well structured, validated input can be used to reduce unintended or unexpected behavior in all software including Ethereum smart contracts. Methods of data validation can be used to produce security for Ethereum smart contracts, with process separation as a priority. Any input from a user to a smart contract must be carefully filtered so invalid or malformed inputs are very likely to be caught. Separating processes would prevent a bug in one part of a smart contract from negatively effecting other parts, a form of damage control. The rule to remember for smart contract developers is summed as "a smart contract must never trust an external input". A variation of this logic must be a basis for any smart contract developer seeking to avoid a DAO like scenario when developing for Ethereum. On Tauchain due to formal verification we could exclude by logic the undesirable behavior so that an external input can produce a limited number of possible states. I admit this might not be easy to do at first but over time the recipes for secure input processing will be part of the Tauchain knowledge base allowing any developer to plug it into their code like a template.
A working Tau will allow for a new form of distributed digital governance
A sentence S divides all its possible interpretations into two classes, those that are models of it and those that are not. In this way it defines a class, namely the class of all its models, written Mod(S). To take a legal example, the sentence
The first person has transferred the property to the second person, who thereby holds the property for the benefit of the third person.
defines a class of structures which take the form of labelled 4-tuples, as for example (writing the label on the left):
the first person = Alfonso Arblaster;**
the property = the derelict land behind Alfonso's house;**
the second person = John Doe;**
the third person = Richard Roe.**
This is a typical model-theoretic definition, defining a class of structures (in this case, the class known to the lawyers as trusts).
Algorithmic stake-based democracy is possible via algorithmic voting. There of course will be problems verifying identity but in stake weighted voting we sidestep these problems. Through eID we can utilize the government to solve the problem by letting them use their digital ID infrastructure to allow for voting or other mechanisms. This is not going to be the ideal solution as governments don't seem to provide great security against identity theft but it is currently the best we can do. Additionally, Tauchain offers the ability to express all forms of legal contracts which can be described in plain English (or any other language) and translated into digital forms. A smart contract could be aware of local laws, international laws, local customs, any set of rules under any kind of predefined logic. Deontic logic for instance can be used as a basis for the generation of smart contracts which have legal awareness and compatibility.
References
Interesting post