Tau Chain

τ-chain (pronounced tau-chain) is a decentralized peer-to-peer network having three unified faces: Rules, Proofs, and Computer Programs, allowing a generalization of virtually any centralized or decentralized P2P network, together with many new abilities, as we present on this note - pdf

For more information see: idni.org or tauchain.org

And here on soundcloud

A DHT is a general scheme for decentralized file storage. Every file has a unique identifier (hash) and is retrieved by it.

Kademlia is a special case of DHT using the cryptographic hash SHA1 and uses an efficient metric (the XOR metric) that significantly speeds up the process of finding a node storing a file given its hash.

Bittorrent is a special case of Kademlia and is the most successful and popular decentralized file sharing network nowadays.

An algorithm for decentralized timestamping, meaning nodes may agree about the chronological order of events without having to trust each other. A blockchain is a chain of blocks, where the next block is accepted by the nodes only if it meets certain cryptographic requirements that imply time ordering (under cryptographic assumptions, briefly described below).

Blockchain's form of storing and transferring the blocks is also a special case of DHT.

A notion of proof comes in some formal system. A formal system consists of an alphabet and rules how terms may be formed using this alphabet. In Euclidean geometry, for example, we have a formal system consists of logic and Euclid's axioms.

A proof of a term (or statement, or theorem) is a sequence of terms that reaches from the given term to some of the axioms, where every step has to be justified by a derivation rule.

The most natural derivation rule is called modus ponens, which says that if A⇒B (A implies B), and A is true, then B is true. This derivation rule can be expressed formally as ((A⇒B) & A)⇒B. Though the perceptive reader might feel some kind of cyclicity on this definition, that touches on the difference between judgements and rules. Refer to Martin-Lof Type Theory literature for more information.

A logical proof is a proof within a formal system of logic, as used regularly in math.

Some proofs are not proofs in the logical sense, but it is customary to accept them as proofs for practical uses. A proof under cryptographic assumptions generally means two things: that we agree on some lower bound of human ability (like algorithms that perform more than 10^86 steps therefore can never be done by human since this is the number of atoms in the whole visible universe), and we agree that some problems are indeed that hard.

As an example, taking a 1MB file and hashing it into a much shorter string, will of course not generate a unique hash (due to Dirichlet's pigeonhole principle), but it is believed (and yet unproved) that generating a file with a given hash is physically impossible. It should be noted that cryptographic proofs can be used only in special cases. There is no way to cryptographically prove "ordinary" mathematical theorems, and they should require logical proofs as customary. Nevertheless, it should be noted that cryptographic assumptions can be considered as a part of a formal system, since they indeed define inference rules.

Any programming language is a formal system, and as such we may ask on its expressiveness, consistency etc. A general model for computation was first given by Turing, namely, the Turing Machine.

A Turing machine is a mathematical object supplied as a set of axioms, and is believed to represent any physical computer (the Church-Turing thesis). So we apparently have maximum expressibility. Is it good? The answer is astonishingly no, and it was Turing himself who pointed it out.

Turing showed that he can derive a contradiction from the definition of his machine. He presented the following question: does there exist Turing machine that correctly determines whether another Turing machine ever halts (i.e. not entering an infinite loop or so)? He then showed that both "yes" and "no" answers to that question derive a contradiction.

Around that time, several such results would change what mathematicians believed for ages. I'll mention here only Godel and Russell. Godel has constructed a question that, as in the Halting Problem, both "yes" and "no" reach a contradiction. For that he assumed an axiomatic system of the natural numbers only, together with the four operations of arithmetic. He then proved that the notion of the natural numbers is undecidable as well!

There are no words to describe the shock among the mathematical community about this discovery. Godel showed that any attempt to formalize arithmetic within a finite axiomatic system will end up either inconsistent or incomplete.

By inconsistency we mean that axioms contradict each other, i.e. can prove a theorem and its negation. Completeness means that every correct theorem has a proof.

Last example, due to its simplicity and strong connection to type theory, is Russell's paradox. Russell is, in fact, the founder of type theory. Russell asked the following question about Cantor's set theory: Let X be the set of all sets that do not contain themselves. Does X contain itself? If you say no, then it must contain itself since we defined it as the set of all sets that do not contain themselves. If you say yes, then again it turns out it must be no, since it contains only what does not contain itself. Contradiction. Obviously, decidability bugged mathematicians and philosophers since those early 20th century discoveries. Many alternative logical systems were proposed, but the most relevant to our discussion is the Intuitionistic logic. But, in those days, it was not clear at all that intuitionism has to do with "better" foundations of mathematics.

When computer science evolved it turned out that computer programs are exactly the proofs we were talking about: every proof is a computer program and any computer program is a proof in some formal system. This result is called the Curry-Howard correspondence.

Later on during the 70s and the 80s, Per Martin-Lof made another huge step by presenting a formal system that is decidable, and when taking it through the Curry-Howard correspondence we discover it can express anything a finite Turing machine can express! He utilized the idea of Dependent Types and showed that using them we can do anything a finite (=real) computer can do, but keeping the logic decidable hence being able to prove any correct statement about a given code. For example, the halting problem is not a problem on our case: not only that the decidability property assures us that we can prove that a halting machine indeed halts, but we also have an explicit algorithm for this. It has to do with Productivity and Totality checks, and the reader is referred to the literature of Pure Functional Programming Languages for more information.

Over the last years Martin-Lof type theory developed to be no less than a new foundation of mathematics under the codenames "The New Foundations" and "HoTT (Homotopy Type Theory)", giving rise to the development of new math with the new foundations, and this time, when the computer is a participant just like us.

Tau client contains an automated theorem prover that is compatible with Martin-Lof type theory. Every mathematical or, equivalently, programmatic statement can be proved. This allows supplying code with proofs: a proof that the code meets formal requirements or admits safety measurements. We already saw that under undecidable systems, proving "yes" doesn't mean we cannot prove "no". But under our decidable logic, we can prove exactly all true statements. Under the Curry-Howard correspondence, mathematical and logical statements (which become identical on Tau), are code in machine language and vice versa. The prover is able to reason over the code as over any other dependently-typed formal system, and either generate desired proofs or verify them.

Taking this a step further, and employing verifiable computing architectures such as Miller's lambda-auth, we can create and verify a proof that a machine executed the steps it was expected to execute. This of course has far going implications on a decentralized and trustless environment. Tau merkle-izes the execution tree and provides a proof as in lambda-auth.

As known, Ethereum's language is Turing complete, hence there is no sense of proof over a code or over their formal system, since as we saw, sometimes we can prove both "yes" and "no" as in the halting problem.

Ethereum is designed such that all nodes execute the contracts. It does not fit uses where many nodes running exactly the same code is unneeded, hence only admits a narrow section of uses mainly at the form of programmable contracts.

Tau gives a full programming language that is designed to be general purpose even locally and not necessarily in a network. We can see why dependently typed languages (equivalently, pure functional programming languages) are important, due to their decidability on one hand, and practically maximum expressiveness on the other. Existing such languages are Agda2, Coq and Idris (the last one is general-purpose), though they are hard to learn and far from the intuitive structure of "subject predicate object" as in Tau. Tau takes RDF languages (like Turtle, Notation3) and gives them semantics to boost them into fully functional languages.

The protocol of the network cannot easily be changed. If, for example, we'd like to change the block time or block reward, we'll probably have to perform a hard fork. The client, as the protocol, are fixed.

Tau's client is a reasoner that can take a knowledge base and ask "what should I do now" (this is completely equivalent to being the automated theorem prover as above). So the client downloads its own "directions" from the blockchain and follows them. The current block should also specify the acceptance conditions of the next block.

Tau reasoner contains builtins that let it perform DHT and blockchains operations. Rules can direct the client to perform such and hence communicate with other nodes, still trustlessly being able to authenticate both data (by DHT hash) and its time (by blockchain timestamping). It should be mentioned that Tau's logic natively supports “contexts”, meaning, there is no "one ruleset" - anyone can create a new context and operate separately from other ones. Still, they may reference existing contexts and reuse their code.

Below we elaborate more on Tau's features and properties:

Tau is the first dependently-typed programming language that is considered human-readable. We take existing languages (RDF family like NQuads, Notation3) and give them semantics to perform as a general computation language.

It is also the first programming language that contains a blockchain support built-in. Building a decentralized application over Tau is natively supported and is in fact Tau's goal: to generalize the concept of decentralized applications to the highest degree possible. It’s also worth mentioning that Tau is a multi-lingual programming language: ontologies can be written in English or Chinese or Russian or even a language you invented yourself, as long as it keeps the subject-predicate-object structure and aliases Tau's builtins.

Tau is also like a decentralized GitHub, but with far-going abilities thanks to the decidability of our type-system (which does not exist in Turing-complete languages).

This allows an ultimate code reuse: if you want some function or piece of code, you can formulate only the requirements of that function, and if a matching one already exists in Tau's codebase, you can easily find it and use it.

Now what if there isn't such a function yet? Over Agoras one could set a reward to whoever implements those requirements. Because over Tau one can supply (and generate) a proof that a code is meeting requirements, the whole process does not require trust.

Tau is also like a decentralized Appstore. It allows running apps from the Tau-chain. Thanks to the type-system we're able to offer another revolutionary feature: one may choose to run apps only if they have a proof that they are safe! Since on Tau one can prove or disprove any claim regarding a given code without actually running it, various security requirements can be chosen and provably cannot be broken.

It is also possible to prove execution and not only requirements. One is able to supply a proof that a code was executed on their machine as expected, i.e. provable/verifiable computing (See Miller for further information).

Tau can also be seen as a decentralized and collaborative democracy and rulemaking system. This goes from formulating rules, obeying them (as long as a computer can obey such rules), and voting for them in any vote mechanism the users themselves choose. Moreover: one could query the laws with the reasoner and find conclusions and inconsistencies in a rule system. One could also supply an explanation that can be automatically validated. Hence, for example, even trustless arbitration can take place, where the arbitrators have to give a formal explanations to their decisions.

The economical implications of Tau and Agoras cannot be exaggerated. Tau is able to incentivize itself: the users can set any rule to incentivize any participant by some conditions (the simplest example would be a mining block reward, though it can be anything and can be changed with time unlike in traditional blockchain). Tau also opens the door for global computing resource market with scales of storage and general-purpose computational power never imagined. Also human services can be given over the network, as I described wrt Bitagoras - github

Even with not-so-many users, Tau network will be able to download virtually the whole internet, practically giving everyone the same information Google has, and more: data can be queried and processed more meaningfully and collaboratively, so you could perform queries as you like. Imagine how your search would look like if you had the whole of Google's database! The futuristic search engine I've been talking about the past year is going to take place over Tau.

Another example of a nontrivial usage is the ability to find implications across sciences: one math problem might be isomorphic to some chemistry problem, and such correspondence can be easily detected and used over Tau.