RE: What Tauchain can do for us: Effective Altruism + Tauchain
Yes, I subscribe to effective altruism. I remember you asked in our last conversation about how do we decide what the well being for all is. I suppose being familiar with this theory the answer would be all life to the extent their consciousness can experience happiness/suffering.
Of course this definition of morality itself can't be justified by first principles, as we run into the wall that is Hume's famous argument generally surmized as 'you can't get an ought from an is'.
What I'm intrigued to know is how can a programming language written in complete and consistent ontologies at the cost of expressiveness grow to become far more powerful than current Turing complete (but inconsistent) machines?
Even more modest utilities like bug free software via the ability to foresee all possible consequences before running the code seems very unintuitive, but how come powerful AI arise from this language?
This is not a challenge, I'm genuinely intrigued and am asking out of ignorance. I suppose to all the lay men and women out there, we can bearly fathom a complete and consistent language, let alone draw a straight line from that to it's applications.
Can you give us a basic understanding of what the utilities and applications of a fully decidable language are and how it fundamentally differs from conventional languages in application, and what sort of expressiveness did you have to sacrifice to enable completeness and consistency?
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.