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.