RE: What Tauchain can do for us: Effective Altruism + Tauchain
You will be surprised once the Tauchain Meta Programming Language paper is released. It's not restricted to only one grammar, or only one logic. Under a certain logic it is decidable over infinite trees but this is not under every logic. In specific you get plenty of expressiveness with MSO (monadic second order logic) far beyond anything else out there. N3 (Notation 3) for example can be used for knowledge representation but you cannot quantify. So you cannot under traditional N3 have the ability to have the expressiveness of the modified N3 which is likely to be included in the Tau meta language.
Details are left out because research is ongoing and it's not completely written down but the main outline is complete and I'm going by what I understand of that. The traditional Tauchain (calling itself Autonomic) is forked and will be the version you're talking about with the limited expressiveness. The updated Tau language does not have limits and while Tauchain will have necessary limits for security and safety it will not be the case that the offline (Tau Meta Language) has these limits.
A problem with the traditional Tau design (Autonomic) is the fact that it requires experts. In order to program over that you will need programmers who can deal with formal verification and obscure tools. This puts a bottleneck in terms of knowledge diffusion and can lead to a technocratic situation not unlike what we currently see in Ethereum and Bitcoin. The updated Tau will do the verification and program synthesis in the background level so anyone can take part in collaborating on a formal specification which the automated programmer (program synthesis) will turn into code. This makes a huge difference when you want to scale quickly, or handle big projects/programs, with thousands of people contributing to the spec almost Wiki style. In short, I'm not sold on Autonomic because I don't think the original Tauchain design will scale.
For more on Autonomic:
And for important concepts behind the updated Tauchain design
If you continue to find these topics interesting I would suggest you have a brief conversation with Ohad Asor. He is the only person with a full and detailed understanding of the intricacies as it would take myself months to catch up with all the papers he has studied. I can however suggest one particularly excellent presentation which is my personal favorite on the subject and if you can grasp the details in that then you'll be able to understand the Tau Meta Language rather easily: Presentation//... and extremely detailed!! associated thesis//
I have talked with Ohad, he gives quite robust answers. I feel sort of bad taking up his time as I know he's the sole developer of this project which is why I'm reluctant to take up his time.
I don't understand the programming side of it at all. From my limited understanding of Godel's theorem, a system of representation as expressive as Peano arithmetic is either incomplete and inconsistent. So turing completeness for example is complete but inconsistent. Tau is attempting to build something that is both complete and consistent and to do that it has to sacrifice some expressiveness.
Now there seems to be multiple logics running through Tau, I wonder if each of them are both complete and consistent and are sacrificing different parts of expressiveness. If they are either incomplete and inconsistent, it would not be decidable in the consistent sense and therefore sort of pointless. This is basically Ohad's main disagreement with HMC on bitcointalk forums causing Ohad to abadon MLTT for MSOL as the former wasn't quite complete.
I'll limit my msgs to him to under once a week hehe, I'll see how he responds. I'm surprised that complete and consistent programming languages aren't already ubiquitous if they offer this great an advantage though.