First, thanks for the compliment by saying I deserve more up votes. 

Now to give some clarification on the security mechanism of Tau as I currently understand it. Tau offers language security constraints through logical consistency.

![enter image description here](https://upload.wikimedia.org/wikipedia/commons/thumb/5/51/Square_of_opposition,_set_diagrams.svg/2000px-Square_of_opposition,_set_diagrams.svg.png)



![enter image description here](https://upload.wikimedia.org/wikipedia/commons/c/c6/Argument_terminology_used_in_logic.png)



![enter image description here](https://upload.wikimedia.org/wikipedia/commons/thumb/2/29/PeirceAlphaGraphs.svg/1142px-PeirceAlphaGraphs.svg.png)



An illustration would be if you take propositional logic and you look at a truth table and you know that at the end the result always must be True or False. It can never be both True and False. There can never be a contradiction or it could not be called logically consistent. The first practical benefit I can think of is that with Tau you do not have the halting problem anymore. This would mean Tauchain does not need "gas" as a way to avoid a smart contract running forever. Gas works to make sure all smart contracts on Ethereum can terminate but when you use Tau your termination is guaranteed because all smart contracts would be decideable. Decideability again is explained by propositional logic where with a truth table you can always be guaranteed a TRUE or FALSE at the end and maintain a result which is always logically valid. These are just the first two distinct differences between Ethereum and Tau but now I'll discuss some more wider implications.

On security when you have logical consistency then the entire set of steps from input to output in a program can be determined in advance. The behavior of a program is predictable, quantifiable, exact, and you can use formal verification to guarantee that every program executes exactly in the predefined way. This is what in information security circles is called "Security by Correctness"  while with Ethereum you have "Security by Isolation".   When you deal with a smart contract which is Turing complete, undecideable, then you cannot rely on logic to predict with certainty how the program will behave prior to running it. What this means is a program will look like a black box with an input on one end and an output on the other end. You do not have a way to know what goes on in the black box so the only way to make sure the program is safe is to carefully craft your input and analyze the output. You cannot rely on logic to protect you from unintended behaviors.

If we look at a smart contract then what the attack did was an input which produced an unexpected behavior. The input was valid to the smart contract because of some unknown bug or feature (the black box). But the input was deliberately crafted in such a way to exploit a common error that smart contract programmers make in Solidity. This puts the advantage permanently on the side of the attacker in the Ethereum ecosystem because the assumption is that most programmers are not going to be skilled enough to program defensively, to follow best practices, to formally verify, and so on. As a result this leads some to conclude that Solidity itself is somehow broken or that Ethereum by design is always going to have these problems and that maybe the best solution is to write mission critical smart contracts on a platform designed specifically for mission critical smart contracts. 

Tau is a programming language not a platform. Tauchain is Tau with a unique blockchain data structure. Agoras is an intelligent market place. In Tau if there is a place to make mistakes it is in the formal verification and design stage rather than in the implementation stage. This would mean Tau by design is a defensive programming language in the sense that the attacker cannot really attack the implementation or the code because it would be known that instead of a black box you have a transparent box where all the possible behaviors are mapped out in advance. It's possible to get that wrong and have a really stupid map of behaviors or model but this in my opinion is more the problem an architect faces when they come up with a bad design.

These are two different approaches. Ethereum is easier to develop for with Solidity in some ways in that anyone can hack together a smart contract. Any one of us can go to the Ethereum site and create a democracy smart contract or a crypto-currency and that is beautiful. At the same time you would need a lot of very safe and secure templates which are known to be safe and at this point in time there aren't many and because the language is too new there aren't sufficient robust libraries with generally recognized safe code to draw from. As a result everyone has to sort of go alone and hope they are a good enough programmer to write a secure implementation of a smart contract and the average programmer just isn't going to be capable of this.

![enter image description here](https://upload.wikimedia.org/wikipedia/commons/thumb/1/12/SubjectPredicateObject-GraphRDF.svg/2000px-SubjectPredicateObject-GraphRDF.svg.png)


![enter image description here](https://www.w3.org/TR/rdf11-primer/example-graph-iris.jpg)

Tau on the other hand will be relatively easy to code. Anyone can work with Notation3 so the programming in Tau part will be even easier than programming in Solidity in many ways. The hard part is many people have no experience creating formal specifications, dealing with formal verification, modeling the behavior of software, it's just a different way of thinking about problem solving which for most programmers is unfamiliar. So because it's unfamiliar it's seen as being "hard". Agoras is important because you don't have to be a mathematician if you have enough tokens to pay a mathematician to come up with a formal spec for a design you specify in plain English.  Then once there is a formal spec which is used to produce the "requirements" you can contract out globally to anyone the Amazon Turk style coding responsibility. You can literally reward in tokens per line of code to anyone who contributes a line or you can set up a keystroke lottery or whatever you want.

Tauchain has many differences as well. You have the root context which is at the top of the family tree which all other context branch off from. The main rules of Tauchain are set at the root context. This context defines how Tauchain will define itself. All clients will download this proofchain or treechain (not quite sure how Ohad would explain it), and will run the exact same code which is guaranteed to run the exact same way on all clients all around the world. So you get something which is like a blockchain in that you have a shared state, but you also go much further because shared state literally means something more like the Raft protocol where the code itself or execution of the code itself is part of the shared state. This means it's like a decentralized Github, combined with a decentralized app store, combined with a proof chain or tree, which guarantees all apps behave exactly as defined by decideable logic. For mission critical smart contracts it might make the most sense to code the implementation in Tau, implement it as it's own context with it's blockchain on Tauchain, and through a side chain you can communicate with Ethereum smart contracts. In this way you can isolate the reliable components by putting it on the reliable platform from the unreliable components which could be put on any platform including Ethereum.

 

References
1. https://simple.wikipedia.org/wiki/Halting_problem
2. https://en.wikipedia.org/wiki/Decidability_%28logic%29#Decidability_of_a_logical_system
3. https://en.wikipedia.org/wiki/Black-box_testing
4. http://searchwindevelopment.techtarget.com/definition/static-analysis
5. https://www.youtube.com/watch?v=OLGVhszBlq4

Tau itself is written/created in C++ because Tau is a compiler. All programming languages have compilers. All compilers must be created in an existing programming language. This would mean the Java virtual machine cannot be created in Java. This would mean the Rust compiler cannot be created in Rust. This would mean C cannot be created in C, because you have to program the compiler in a stand alone language to implement it.

As a result the first implementation of Tau will be the C++ implementation. The C++ implementation does not have to be the only implementation. A Turing complete programming language must be used to implement Tau because according to my understanding you cannot put the constraints there. The constraints have to come in after the logic is put in place which happens in the compile process itself not in the compiler executable. This means Tau has to be programmed perfectly, and Tau itself will have to use correct by construction, which is actually possible to do with CompCert the verified C compiler. I do not know if you can do it using a C++ compiler but I know C and C++ aren't so different so someone could implement a C version of Tau with the verified compiler as long as Ohad releases a formal specification. I think also there is EscherTech which offers formal verification for C++ so Ohad might be able to use these tools to make an exact C++ implementation correct by construction.

References
1. http://compcert.inria.fr/
2. http://www.eschertech.com/products/ecv.php

In specific the consensus on heartbleed is that it was caused by lack of bounds checking. This would indicate that language security may have prevented heartbleed from happening. This doesn't mean mistakes cannot be made but it only means it's much harder to make them with certain languages.

My point by bringing up heartbleed is to show that if you use a notoriously difficult language for secure programming like C or C++, and you do not take all possible efforts to make sure your code is correct, such as correct by construction, formal verification, and all sorts of blackbox testing, then it's a situation where perhaps the entire world has to have faith in the competency of in some cases thousands of different programmers. The statistics do not look good when you consider that it only takes one of them to slip a bug in either deliberately or by accident.


References
https://en.wikipedia.org/wiki/Bounds_checking
https://news.ycombinator.com/item?id=7548991