A discussion and description how Tauchain by a non-expert
Disclaimer:
First, I will say do not consider me an expert on the topic of Tauchain, or on the topic of functional programming. My background is in information security and philosophy (ethics). My theoretical knowledge on these topics come from my academic background, years of personal research, and discussions with the developer of Tauchain Ohad Asor. For the most precise description beyond what I offer please refer to Ohad Asor.
What is Tauchain?
Many experienced programmers, computer science graduates, cryptography experts, have a very difficult time understanding exactly what Tauchain is and why it is so important. The purpose of what I'm doing here is to help demystify and elucidate the way Tauchain is currently planned to function. I'll be discussing topics such as logic and it's implications for information security in software. I will be discussing how software is tested and why Turing complete imperative language represents a risk for all smart contracts which attempt to be reliable. I will discuss Notation3 with some examples on how programming in Tau may work and more.
Design is important and Tauchain is well designed
One of the reasons I became interested in Tauchain is that I noticed the developers behind it were willing to look toward the state of the art. I myself read a lot of academic journals and I recognize when developers are doing serious research. In my first communication with Ohad he asked me about Martin Lof Type Theory which at the time I had never heard of. I did not know who Martin Lof was or why he was significant but as a diligent researcher I followed up on everything Ohad said and reached a conclusion that Martin Lof is actually one of the most important logicians of our time. Martin Lof Type Theory is extremely significant and I realized that Martin Lof Type Theory and was slightly related to something I stumbled across in my own research called intuitionist logic. Intuitionist logic introduces the concept of the constructivist proof which in basic terms means you demonstrate by example (demonstrative proof) rather than symbolic representation alone.
A brief explanation of propositional logic to explain the power of decidable smart contracts
In order to understand what Tauchain can do you may need to understand the basics of logic. If you are a philosopher you may be familiar with logic but for those who do not have backgrounds in philosophy I will give a simple explanation of propositional logic.
The basics of propositional logic require an understanding of the logical connectives. For computer programmers you might have a similar concept called logical operators with the if, and, or so it may be easy to follow.
- Conjuction means "and".
- Disjunction means "or".
- Negation means "not".
- Implication means "if...then".
- Equivalence means "if and onlyif".
- Alternative denial means "not both"
T = true, F = false
In addition to these English language descriptions you also have symbols. The main symbols used in a propositional logic truth table are P and Q. I will give a brief example on how this is used .
In a truth table there are 4 unitary operations.
- Always true.
- Never true.
- Unary identity.
- Unary negation.
For the most part I will not go into that.
Onto the truth table.
A logical argument requires a premise and a conclusion. A truth table has either T or F where every statement in the table must either be True or False (T or F).
For each distinct statement we use the letter P or Q.
P: Barack Obama was born in the United States.
Q: Barack Obama is the President of the United States in 2016.
P and Q: T (it is true that Barack Obama is President of the United States in 2016) + (it is true that Barack Obama was born in the United States).
(P∧Q)
Barack Obama is the President of the United States in 2016 only if Barack Obama was born in the United States.
Ony if Barack Obama was born in the United States can Barack Obama be President of the United States in 2016.
Label the first statement P as A.
Label the second statement Q as B.
B ==> A
The second statement being true implies that the first statement must be true. In fact the second statement can only be true only if the first statement is true.
So if you have a Truth Table you can take facts based on what you know to be true or false, and following the rules of logic you derive a conclusion of T or F. Because you can always derive a conclusion of T or F to any statement you maintain logical consistency. It is this logical consistency which allows for decidable computation but in order to get that you lose completeness. It is for this reason that Turing completeness is undesirable if you want to rely on logic based language level security. Logic based language level security takes the burden way from the programmer in having to concern herself with secure programming or defensive programming because the language itself is defensive and the security is obtained by logical consistency. It is simply not possible for there to be a logical contradiction so if we go back to the Obama example it is simply not possible for P to be false and Q to be true yet B implies A. Barack Obama is President of the United States only if Barack Obama was born in the United States otherwise you have a logical contradiction which renders everything meaningless.
Turing completeness allows for these sorts of contradictions. Instead of yes or no, true or false, you get yes and no, true and false, which are meaningless outputs. This causes the computation to essentially never end. It goes on for infinity because Turing completeness goes with the idea that there is infinite memory and infinite time. All current knowledge of the universe reveals the exact opposite and shows you have finite energy which cannot be created or destroyed. This too implies information cannot be created or destroyed including the information which falls into a black hole and escapes in the form of radiation. Godel's incompleteness theory proves that the universe does not allow for both completeness and consistency which reveals something about the nature of the universe as well as the limits to what is computable.
The importance of Curry Howard Isomorphism reveals that programs are proofs
And if programs are proofs then smart contracts are proofs because smart contracts are programs. Logic proofs are the core of all programs and decidable programs are logically consistent proofs. This is something to remember for understanding why Tauchain is based on rules and how it works. It also explains something fundamental about how Tauchain can be able rules, knowledge, proofs, because the rules are based entirely on logic, the knowledge is that which is proven true, the proofs are possibly demonstrative (constructivist proofs). When you piece this all together you have the triad in Ohad's whitepaper where the logic allows for the correct derivation of the proof from it's axioms/hypothesis/premise.
Soft computing/soft coding paradigm
Softcomputing:
When looking at smart contracts or software in general you have two different paradigms. Soft computing is a paradigm where approximation, imprecision, and inexact solutions to computationally hard tasks are deemed acceptable. An example of soft computing is using a genetic algorithm to evolve a solution or if we want we can look at Maidsafe/SAFE Network to see it's using a soft computing solution where you do not have a blockchain data structure at all and instead you have a modified ant colony algorithm. The Bitcoin blockchain itself is also part of the soft computing paradigm because there is no possible optimial solution to the Byzantine generals problem. This is because the CAP thereom shows it's logically impossible to have more than two out of the free between consistency, availability, and partition tolerance. In the research phase it helps to learn what is impossible prior to beginning development. Satoshi Nakamoto relies on mining which is NP hard, and distributed consensus is a problem which no algorithm can ever efficiently solve. Maidsafe and Satoshi Nakamoto rely on the soft computing approach toward solving the problem because there is no algorithm which can give a precise solution.
Softcoding:
Soft coding is a much safer and smarter design pattern. Any commonly altered value should be soft coded. Soft coding promotes freedom and customizability. The software which is soft coded is better able to conform to the wishes of the user. Tau takes this to the extreme where the Tauchain network is entirely self defined. It is autopoietic in the sense that once it's completely set up and particularly running with Agoras it will be self organizing and self maintaining as well. Tauchain will be whatever it's first users want it to be. Tauchain is as flexible as possible which is good for freedom.
Hard computing/ hard coding paradigm
Hardcomputing:
Hard computing on the other hand can contribute to over engineering because some problems can't be solved through hard computing because no efficient solution can ever exist. Decision analysis, preference aggregating, and decision making are NP hard problems in the sense that you cannot rely on the perfect algorithm or any kind of exact hard computing. In essence you can only solve these sorts of problems with soft computing which means you can use blockchains, swarm intelligence, voting, all which are soft computing. Tau in specific avoided this by going with the blockchain data structure (tauchain) and self defining nomic for rules.
Hardcoding:
Hard coding is a common antipattern. Hard coding allows for and contributes to many programmer errors. Tauchain starts with no rules at all in the root context which means it's not hardcoded at all. The first users will have what seems like unlimited flexibility to define Tauchain. This means Tauchain potentially can always maintain alignment with the self interest of the community who set it's rules and in cases where the community may disagree there is no forks. Instead of forks it is very simple to simply create a new context and spin off from there so that everyone gets what they want with context separation. The issue with Bitcoin or with Ethereum deciding to fork or not to fork would be rendered irrelevant on Tauchain.
A brief introduction to notation3
Notation 3 is based on the concept of subject -> predicate -> object. It's unique in it's simplicity yet it's powerful enough to describe anything. Notation 3 allows the programmer to become an ontology engineer and describe by subject -> predicate -> object what I can best describe as a logical graph.
How-to-Tau
Let's begin with an English sentence: Alice knows Bob.
The subject is Alice.
The predicate is knows.
The object is Bob.
In this case the predicate describes what Alice does or is. Knows is something Alice can do because Alice is a human and a human has that ability. Bob is a human also and can know Alice. This reveals that there is logic in the background which we will discuss later but first let's have a look at the code.
Example of Notation3 code below:
@prefix ppl: <http://example.org/people#>.
@prefix foaf: <http://xmlns.com/foaf/0.1/>.
ppl:Alice foaf:knows ppl:Bob
The code above uses the 
Example of a rule below:
@prefix ppl: <http://example.org/people#>.
@prefix foaf: <http://xmlns.com/foaf/0.1/>.
{
ppl:Alice foaf:knows ppl:Bob.
}
=>
{
ppl:Bob foaf:knows ppl:Alice.
}.
Remember propositional logic? Logic is the basis of rules in notation3.
The "=>" means implies. If this then that. Expressed succinctly it states if Alice knows Bob then Bob knows Alice.
To say it another way, Alice knows Bob implies Bob knows Alice. This becomes a rule and once you make it a rule in notation3 you can reason based on that rule knowledge. Tau will have a reasoner which can apply deducative reasoning automatically to deduce additional facts from the knowledge graph. For example if Tau knows what a human is, and knows all people are human, and all humans are mammals, then it can figure out that Alice and Bob are mammals if they are human using deducative reasoning. This is very powerful for programmers if used appropriately.
As you can see the basics of notion3 are not hard and while a basic understanding of logic may be necessary it's not very different from the logic people expect with conditionals in traditional programming languages. What is different is that you have automated reasoning. You describe how a program should function rather than tell it through step by step commands. As Tau grows it's knowledge base will grow, and you will be able to query Tau itself for code snippets to reuse. You will be able to know exactly what it will do and programming will get easier over time.
Why Turing complete smart contracts are dangerous
When you deal with software which is not at decidable there are ways to try to make it somewhat reliable. All of the best known methods rely on black box testing. It's called block box testing because we first have to recognize that we cannot know with certainty what goes on in the black box. We only can work to be careful about our input and analyze the output.
When you're dealing with a black box you're dealing with undecidable logic. When you're dealing with a black box you're dealing with a situation where it's possible that you could experience unexpected behaviors which can lead to unintended consequences to the participants in the smart contract. In order to create a secure smart contract using a Turing complete language you have to be extremely careful to defend against crafted inputs while at the same time you have to analyze the outputs. It can take many years of testing before you get software which functions how you think it should function unless you can figure out what goes on in the black box.
Why reliable smart contracts on Ethereum may be impossible and a choice between reliability and immutability may be inevitable
Ethereum smart contracts currently are unreliable. Many security researchers and highly competent individuals say that on a fundamental level these smart contracts will never be reliable. In my opinion while it may be possible to create reliable smart contracts it is not possible to do it consistently with the current tools and it would take a complete rework of Ethereum to address this situation by putting in place at minimum mandatory formal verification which still might not be guaranteed to produce perfectly reliable smart contracts but would be better than as it is now.
The issue with Ethereum comes about from the fact that it requires reliable smart contracts to be valuable at all. It's a valuable platform based on the fact that it offers what people expect to be reliable smart contracts. It is valuable based on the fact that people expect that because Ethereum is decentralized that it will be more reliable and more secure than centralized. The DAO hack exposes the fact that smart contracts are not reliable and maybe it's actually no more secure than the centralized web.
Immutability is a desired feature because people want to know that smart contracts will potentially live forever. I will have to say immutability is a similar ideal which will not work in practice just like Turing completeness requires you do not have consistency the fact is that with Ethereum it may be desireable to have immutability but immutability without reliability is worthless.
If there are smart contracts which are both unreliable and immutable then you get the worst of combination. You get the insecurity and you also get something dangerous which would be run-away smart contracts which can't be shut down even when the majority of the planet thinks it should be. For this reason in the end Ethereum will probably have to sacrifice immutability for satisfactory reliability. Satisfactory reliability means if there is a bug in a smart contract then there can be a process to hard fork and restore funds or if there is an unjust confiscation they can undo and restore.
Tauchain is so far the only platform which will guarantee reliable smart contracts
Tauchain can guarantee reliability for smart contracts because of the formal methods used, the fully functional dependently typed programming language, the Agoras which will be able to purchase computation, storage, and even code itself, from an intelligent market. If there is to be a billion dollar smart contract it is likely never going to be on Ethereum and more than likely will be on Tauchain or a successor.
This does not mean nothing can go wrong with Tauchain. It's going to be an extreme challenge to even create Tauchain and Tau the programming language may take years before people can understand the value. Last by not least it is possible that people will go with what is trendy rather than what is reliable and in this case we may have a future where people store billions of dollars in backdoored smart contracts which get seized back and forth by hackers but I would hope Tauchain offers the alternative for people who care about mission critical smart contracts and serious experiments which require guaranteed reliability.
References
- https://en.wikipedia.org/wiki/Softcoding
- https://en.wikipedia.org/wiki/Propositional_calculus#Basic_concepts
- http://tauchain.org/tauchain.pdf
- https://www.w3.org/DesignIssues/Notation3.html
- https://www.w3.org/TeamSubmission/n3/
- http://www.thoughtclusters.com/2007/08/hard-coding-and-soft-coding/
- https://en.wikipedia.org/wiki/Anti-pattern
- https://en.wikipedia.org/wiki/CAP_theorem