This is all interesting..

Just to rehash this....

After time has passed is opinions the same?

Has there been a closing of the gap with disagreements or are opinions still varied?

Quote from: HunterMinerCrafter on September 27, 2016, 08:21:48 PM

Quote from: cryptico on September 27, 2016, 04:23:21 PM

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.

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.

Quote

MLTT does not have decidable typecheck in general.

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.)

Quote

But it is not the case that everything expressible is decidable.

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.

Quote

This situation led me to a conclusion that MLTT was a wrong choice, and another logic should be considered.

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.....

Quote

The remedy for this situation is to pick a different logic, a "complete" one.

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"...

Quote

Specifically, certain classes of Monadic Second Order Logic (MSO or MSOL) were found to be complete and consistent since the 1960s, but they did not have satisfactory expressiveness abilities.

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.

Quote

To mention three advantages: the existence of a direct computational model, the ability to infer programs, and simplicity of use.

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.

Quote

It cannot possibly exist since automatons are an explicit finite decision procedure, while dependent types are not completely decidable.

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.

Quote

This task is undecidable on MLTT

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

Quote

We can have correct-by-construction programs and contracts, by merely stating what we expect them to do, and commanding the machine to find such a structure that admits our requirements.

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.

Quote

MSO logic is simpler to use for the reasons mentioned above: it is a simpler language, and does not require human intervention to convince that a true statement is true indeed.

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.

Quote

It also represents a more intuitive logic:

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.

Quote

More formally, intuitionistic logic explicitly negates the law of excluded middle.

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

Quote

And this is of course highly unintuitive, and allows the possibility of human mistakes especially over complicated structures.

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.

Quote

On the other hand, MSO is a Classical logic, means it includes the law of excluded middle: it's simply impossible for anything to be both true and false at the same time.

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

Quote

The middle is completely excluded, while if we add this rule to MLTT, it loses its consistency.

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.)