As a non-programmer and non-mathematician, I've been looking into tau for a few days, trying to understand what it's all about. It's really hard with the lack of education that I have, and it seems that it is hard for programmers too.
The benefits of decidable programs just don't become obvious to a layperson like me as long as the talk is at an abstract level, even though the concept is understandable. However, after you mentioned that bugs in software like Tor and OpenSSL are because of intuitionist/turing-complete programming, my eyes started to open to the potential of the project. Thanks!
If I understand it right, it's easier to program in the intuitionist way, and practically all existing software libraries are such. Even Tau itself is being programmed in C++, which I find a little contradictory, but never mind. It seems to me that what the project is doing is starting a completely new ecosystem from a clean table, with an ever expanding library of totally new, bug-free, provable, reusable functions free for anyone to use. It will start off with practically nothing but the rules, and gradually accumulate a variety of libraries, which will make programming for Tau easier and easier. The libraries will provide perfect abstraction; you don't need to worry about the inner workings of it, because it will function consistently, and thus it will be a good platform to build upon. There is a huge uphill, where the benefits are small in the beginning, but which will become massive and obvious over time.
Aside from the long term prospect, there is an immediate benefit from combining consistent programs with a blockchain, namely the possibility to "trustlessly" and automatically validate someone else's code or the results of running a program. This supposedly makes it possible to "trustlessly" outsource both computing power and programming, which hasn't been possible before (?). This will of course open up huge possibilities, and that's where Agoras comes in. Tauchain itself doesn't have a token or a revenue-model, but Agoras does. Agoras needs Tauchain to function, so the creators are crowdfunding Agoras and using the funds to create Tauchain. It will surely take many years to start generating any profit, but the potential is apparently huge.
I think Agoras (AGRS) might be a hidden gem, an investment opportunity, because it is so hard to comprehend. Bitcoin is hard for people to understand, which made it a good opportunity for those who grasped the concept before the masses. So was Ethereum; it was hard to understand and very ambitious, but gave good returns for those who made the effort to understand. The benefits of Tauchain aren't obvious at all, and require quite some thinking to envision, and that is what makes it a possible hidden gem. The hidden-part is sure, while the gem-part remains to be seen. It will take many years to produce revenue, but once people start to see the potential and to talk more about it, the price will likely appreciate. I think I have to buy some. The price is at it's lowest.
You certainly deserve more upvotes. This was a very enlightening article.
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
Ok, so writing the compiler in C++ doesn't necessarily make Tau unpredictable. Thanks!
It's not impossible to write reliable code in C++. It's just very difficult to do it and even when you do you have the problem where the more complex the code is the harder it is to audit. When you use correct by construction, and when your code is limited only to for example a compiler, then you can focus all community efforts on that. You have to trust fewer programmers and fewer auditors when you use correct by construction and build the compiler only in C++ and do the rest in Tau.
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