In Tau you will be able to reason over the code and evaluate it for a proof of correctness.
For me, this aspect is the very essence of TauChain . In one of your first posts you wrote:
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.
So Tau offers a guarantee that the code will fulfill the specification - that's great and I understand it. But what will guarantee that my plain English description is translated by a mathematician into a specification without any errors or omissions? Don't we just move the problem one level up?
Also, have you got any example of a formal spec for a piece of code to be written in Tau or any other provable language? it's hard for me to imagine what it looks like.
From my understanding of what is planned there is a developer or two who will be working on a controlled natural language. Attempto Controlled English (ACE) will allow implementation of something like Attempto for example.
and...
So while not straight up English it will be a controlled English which means anyone who can speak English should have no problem dealing with it.
References