The hard work keeps going, there is still a significant way in front of us, but we already have nice achievements. We finished the core of our Automated Theorem Prover, it works great and beats some state-of-the-art reasoners, while it's not done and going to be even better. We are now focusing on implementing the type system, which is what takes semantic web languages and give them semantics so they can do everything a finite Turing machine (aka computers) can do. Then we write the genesis block, and the tau network will begin its running.
On this opportunity I'd like to mention a few of tau and agoras capabilities, mainly such that haven't seen so far:
1. Programming Language: 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 as possible.
2. Software Development: Tau is also like a decentralized GitHub, but with far-going abilities thanks to the decidability of our typesystem (that 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 typesystem we're able to offer another revolutionary feature: one can 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 (aka provable/verifiable computing).
3. Legal: 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 themseleves 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 arbitrers have to give a formal explanations to their decisions.
4. Economy: 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 (https://github.com/naturalog/Bitagoras).
5. Information: 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 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 isomorphism can be easily detected and used over tau.
There can be many more uses, but if I'd be sitting to write them down, I wouldn't be able to write tau itself. So that's all for now, got to get back to get tau ready for launching.
Thanks for your support!