Topic: Tau-Chain and Agoras Official Thread: Generalized P2P Network - page 102. (Read 309762 times)

I guess we will wait and see if things come out as expected. Everyone should work out their difference, keep egos at check and focus on the project.

We have already had significant public discussion in the IRC channel, which did not lead to any resolutions, but I will still summarize the state of affairs here for you.


While technically true for general MLTT, it is not a problem in practice in an MLTT TFPL, particularly for tau.  If it were generally a problem, languages like agda/idris would not be particularly useful for verified programming.  In the (few, largely meta-theoretical) cases where this does significantly complicate proofs in practice, postulates can be used to sidestep the problems/complexities.  (This was the approach wrt "tau classic" design as well, community-agreed postulate rules within contexts.)

If you restrict "expressible" to exclude meta-theoretic propositions, partial propositions, and non-productive propositions (again, as agda/idris do) this statement is simply false.


OK, let's assume he were right, and MLTT was somehow not suitable - for the sake of answering your actual question of what the problems with the proposed alternative are seen to be.....


As we (the non-Ohad "team" members) see it, tau (classic) necessitates a "computationally complete" language.  We believe this is the case due to the problem statement itself: a fully generalized decentralized network.  In order to be "general" the logic of the network needs to be able to "compute any computable function" in the processing of its rules, as otherwise you restrict the set of possible rules that the network can employ, and lose generality.  Because tau also necessitates consistency (I don't think anyone will argue that point) the requirement of a computationally complete language would imply the necessity of a logically *incomplete* language.  This is largely the central "dispute" between Ohad and the rest of the "team" at this time.

Let's go on to see what alternative logic he did choose, though, to see the "lesser point of contention"...


The expressiveness of MSO is the specific concern.  We do not (even after months of researching and discussion as to if Ohad "might be right") see how the "self defining nomic" that is tau can be expressed in MSO.  Specifically, we believe that such an expression necessitates general algebraic data types, which MSO can not express.  Ohad will be the first to tell you that MSO omits multiplication, but what he seems to overlook is that it also omits "general products" which significantly limits the ability to even express something like a blockchain, let alone a tau.


The rest of the "team" actually got "luls for days" out of this line.  MLTT has a computational model, has a term inference procedure, and is only slightly harder to use than, say, Haskell or OCaml.  If these things were not the case then the MLTT programming languages and proof systems simply would not be.  As it is, they not only are, but are the most common and popular form of verified programming today.


Again, true of general MLTT but not true of an MLTT TFPL, which omits metatheoretic, partial, and non-productive expressions.  Such a language does have a direct automata translation, which is even employed in the "backends" of some MLTT based systems for efficient code generation.


Actually, it is "semi-decidable"....


Being semi-decidable, an MLTT TFPL can employ this as well.  The only difference is that instead of being a strict decision procedure, it will come back with either a program, a proof of impossibility of the program, or a question about a refinement to our specification.  After a finite number of such questions, it will come back with either a program or a proof of impossibility.  As term inference is an "offline" process in tau usage, this semi-decidability is acceptable.


I don't see MSO as particularly "simpler," myself.  Further, given an "already expressed" proposition and its proof, no human intervention is required to convince an MLTT framework of it, either.  These statements seems entirely disconnected, and do not really follow from the prior line of reasoning.  Which is "simpler" is subjective and debatable. Also, in *any* type system, something that passes typecheck passes typecheck, so I'm not sure what is really trying to be said on this latter point.


Whether classical or constructivist logic is "more intuitive" is a highly subjective matter.  Personally, I find them rather equally intuitive.  I've also spoken to people who reject classical outright as non-intuitive, and people who reject intuitionistic outright as non-intuitive.


Erm, no.  It does not have "not (p or (not p))" as an axiom, as this statement would suggest.


I'm not sure what this is intended to mean.  Although "LEM" is not axiomatic in MLTT, neither is its negation, so it can always be assumed as a lemma for any given proposition.


Being consistent, this is also impossible under MLTT, of course.


MLTT only loses consistency if LEM is included as axiomatic. LEM can be freely applied over any proposition, otherwise.  This is generally so well understood as a "basic concept" in the intuitionistic logic that Ohad's apparent misunderstanding of it has led some of us (myself and stoop, in particular) to question some of Ohad's grasp of the fundamentals of constructive intuitionistic logic, in the first place.  (I'm particularly baffled as to how he can seemingly grasp Glivenko and the Godel-Gentzen negative translation, but cannot grasp the simple matter of the usage of LEM in MLTT.... it seems to me that to understand the one means to understand the other.....)

IN SUMMARY:
The first part of this argument is not really "new" or unique to tau's situation.  The question of "general suitability" of intuitionistic logic goes back to the 1920s.  I doubt that we will resolve this debate, but suffice to say that Ohad is the only one from the "team" who believes that MLTT is unsuitable specifically for tau.

IMO, the second part of this argument is the much more central matter:  Can MSO be used to construct a tau at all.  Nobody else from the "team" seems to be even remotely convinced that it could, and everyone (Ohad included) seems to have a strong understanding and agreement that if it can (at least to some degree) then there is a necessary loss of generality in doing so, which means that the original goal of a fully generalized overlay network would not be able to be met by it.  (This latter point can be easily seen by the fact that MSO is a strict weakening relative to MLTT - anything provable in MSO is provable in MLTT, but the reverse is not true.  This means that there are some rules/topologies which could be enacted on tau classic which could not have parallels on mso tau.  We see this as a *big* concern.)

Hello HMC I can see that Ohad put recently a detailed blog post on why he thinks that the old model for tau will not be working for what tau is meant to be in here:

http://www.idni.org/blog

Can you clarify which part of this post you do not agree on so that maybe you can have a public discussion with Ohad about this? I hope that a public discussion on the ideas and concept is welcomed and can benefit Tau design at the end.

As an Investor I always have seen ohad very open to feedbacks. Since I know you have contributed since the begenning of this project I would like to hear your opinion on why do you think Ohad is making a mistake based on a critique of the article above.

Thank you.

I think that all of us who follow and are invested in the project have a difficult time with this last phase in which the two main developers Ohad and HMC are in such disagreement regarding the further development of this project. However we should bare in mind that this all is the outcome of their deep personal commitment to create the tauchain in the best possible way and their "dispute" is about the logical and mathematical foundation of the language in which the tau should be written. We should  feel blessed for putting our trust in such hands (minds).

 

If you are on Facebook, make sure to join the Agoras Tau-chain page!

They just posted a nice update on the progress made recently.

https://blog.omni.foundation/2016/09/21/state-of-the-layer-all-hands-sep-20-2016/

Yes it would be great if you could explain it here

What were the concerns that you guys had that Ohad didn't agree with?

You nailed it with this one. I entirely agree with you, I think Ohad has the right idea. I also commend HMC for offering their commitment to the project. You can't beat loyalty, especially in a startup environment.

I trust Ohad completely, if he says that after deep investigation he found that the old design will not serve the project's purposes as planned or to the fullest, and that there is a preferable design to use, I fully back him up on this. I get the feeling that there is an ego issue here to some extent. I am certain that there was no real reason for Ohad to switch to a new logic if he did not truly believe that it is the right way to go. I am also certain that the project will move forward with you or without you. I know that some people see you as an expert and for this reason it will be positive if you do decide to continue cooperation with the project in the future. Of course, this is mainly up to you.

Well, the very short form explanation is that nobody on the project except Ohad believes either that there is any problem with the originally planned design, or that his new plan is even suitable to construct a "useful" tau.  During discussion of our concerns, Ohad "went off" on the most active developer (stoopkid) and kicked him off of the project.  Every other member of the "team" (including myself) then basically stopped development and effectively left the project.  This means that Ohad has now effectively lost his second team entirely, and is once again on his project alone.

To my knowledge, in the time (months) since, no new development has occurred.

I still keep my commitment to Ohad to attempt to verify any implementation which he brings forward.

I'm also still happy to explain the original design premise to anyone who would like to know about it.

Initially all i asked was can this token fit into c-cex.com -the answer was "YES"

I still hope the founder does it as it is more than likely it will be accepted there.

And as i see from HEAT LEDGER it will get more activity than on Bittrex.

Then some of the community shits on the idea.

Why? Becasue it is uncouth?

More exchanges the better, more publicity the better. more financing the better.

Then the devs get the finance and get the time and talent to make it HAPPEN.

Here is my mind set.

Can i easily throw my resources at TAU or a close comparison MAID.

Maid is ten years in the making TAU i am not sure.

I get some differences but who knows as even now the foundation logic language has been dispelled.

All good i say, go to the best.

MAID went from C++ to RUST.

TAU is also growing in its maturity and admitting it needs to alter course.

BUT..

its public financing and growth in people numbers can occur while this is happening.

Again i would suggest there is no downside in more than ONE exchange offering the token..


----------------------
https://c-cex.com/?id=vote#suggest

Simply fill out the form
-----------------------------------

Hello! We have 2 options: 1 - You can add the coin on the voting page - https://c-cex.com/?id=vote . We will surely consider adding it if it gets enough votes and the community shows enough interest. 2 - We can list a coin or asset for 3 BTC immediately. Have a good day! Let us know if there is anything else we can help you with. Thanks!

Fully Agree!   Looking at Bittrex, i see the price has been bought up to 27K   as more and more people learn about the "futuristic"  (i think is an appropriate word) developments happening, the more the coin will grow, which is great for investors and developers, its always nice to see your hard work and dedication get the recognition it deserves in reflection of the price.

Looking forward to the Tau-Chain release, which i believe will be the next and biggest release?


Also. NOTE: To anyone wanting to ask questions about Comparing this project against others.

There is a really simple answer to this.  Simply, You cant.  
So please dont ask, there are a couple of videos, pod casts with Ohad talking about the whole project, i will try and find link, its amazing to listen to and will make you understand more, although it is highly technical and advanced whats happening here, i am not ashamed to hold my hands up by saying i only understood about 30% of what was said.

It's completely different than those. It's more like a super computer, and the storage is not to store videos and pictures, but rather rules.

Also is there any clear write up on how this project is different from MaidSafe and Synereo?

They seem to be very active with a lot of Devs.

Will Tau Chain be like the Wolfram language?

the team is very busy working on proyect. and well financiated, dont see the reason to add the coin to other exchanges at this moment and waste his precious time helping to install wallet and explain to use it etc... BItrex is working fine at this time.

Personally I like the way the site looks. It's straight and too the point about the technology and Ohad's thoughts, without all the bells and whistles and animation. It just has a feel of like Ohad legitimately working and believing, vs lets say a scam coin paying someone for a flashy website.

his status is up to him. he's welcome to collaborate on tau as much as he wants, and was always so.

What is the status with him?

Poloniex will ask what special features this coin has EG: what makes it special/different.  This is the most highly technical coin i have ever seen, i really would not know how to answer this.

Would be great if there was a web designer here also, could really do with a nice looking website.