Hi Klosure!
To clarify, what I was talking about in my git analogy was graph contexts, that is to say the semantic space denoted by a
named graph or the fourth element of NQuads or the bNode of a reified statement. These are key to enable the "anyone can say anything about anything" vision because what is stated in a context isn't being stated in the default / most general / objective context.
Yes, Ohad's reply was a bit unclear on this point. I think he has been trying to keep the discussion quite simple, when the answers are unfortunately not quite so. (This is also why I generally prefer our real-time discussions in the irc channel. We find ourselves re-answering the same questions more often, but it also takes less total time in "back-and-forth" to communicate all of the relevant particulars of a topic.)
Tauchain operates over rdf quads, so context is as you describe, named hyper-graphs. However, we make a few particular constraints beyond the standard rdfs (really "lbase") semantics. Every context in the system carries not only a name (which may be "local" as in a bnode) but also a parent context reference. These parent context references form a hierarchy (acyclic) up to the "root context" which is the global background graph of the root chain's logic. We make this additional constraint over the normal semantic web model in order to align our data storage model to our type system's logical module model (cumulative, dependently typed records) which I'll say more on below.
Ok, here that seems to be named graphs you are talking about. You could consider IRIs as pointers that can either point to actual data (URL) or to non-existent / out-of-bound location (IRI without actual web resource) and throw an exception upon trying to access the resource (need to determine how you would represent an exception though).
Tauchain employs a two-phase reasoning cycle. In the first phase the reasoning is closed-world and dependently typed. Anything inaccessible is considered false, and any failed dereference is considered as an inconsistency. This phase is used for checking block validity, reorgs, peer relations, authenticated logic, etc. and is at the heart of tauchain's operation. The second phase, used for reasoning operations that are "off-chain," handling of side-band communications/processes, or are simply "unsafe" (like FFI) uses a more "traditional" (for semweb) open-world and simply typed logic.
You could also keep the POST / PUT / GET / DELETE semantics of HTTP to allow to modify resources when writeable. This will be needed when a context is used to store or manipulate program state (which will be the case all the time). The nice thing of URLs is that, as your Tahoe-LAFS example shows, they can be made to point to anything so Tau would be able to work with stuff stored anywhere: the SAFE network, the upcoming Ethereum Swarm, HTTP etc.
We don't exactly want HTTP semantics, mainly because of a lack of referential transparency. We desire our kb to have certain properties: referential transparency, controlled partial-immutability, monotonicity, and strict positivity within the data model. Again, this is to support a consistent type system. Instead of "crud operations" we use a stable assertion semantics. New data/logic is asserted into a context as facts/rules. Consistency of these assertions are enforced, meaning an assertion must be consistent with ("allowed by") earlier definition within that context and its parent contexts' established logic. (In other words, whenever a transaction means to insert new data into a context that transaction itself must first be deemed "OK to insert" by a query to the existing rules of that context as a challenge to the transaction.)
We do not allow any explicit retraction, and do not allow any direct negative assertion. Instead, we use (weak) negation-as-failure for both constraint and consistency maintenance. When a new incoming rule both explicitly "implies false" and is successfully allowed into a context by the established rules of that context, any direct contradiction to the implication already existing in that context are considered as having been removed from the context from that transaction on. In other words, asserting a new constraint that is accepted into the context serves as a facility for "deletion" of any existing data that violates the new constraint.
By this mechanism we do not need separate "CRUD operations" and can keep the knowledge-base as simply a tree of append logs, with nodes per-context. This simplifies the merkle processes for both the chain management, and the authentication model.
I think we need to stop using that "it will be up to user defined rules" narrative because although it is true, it doesn't preclude the fact that the initial Tau Chain will have to be a fully specified and functional system long before the envisioned power-users come and change everything.
HEH. Ohad's response here was a bit of a social side-effect of one of our (perhaps seemingly "strange") beliefs about our work. We very strongly desire to avoid biasing our "experiment" at all costs, and this means that we intentionally avoid public speculation or commentary on certain aspects of how we "expect" the chain to be managed. Further, we strongly believe that it is neither our place nor our right to make these decisions prior to genesis. These concerns are for the "future tauchain user people" to address, and indeed finding the "best way" forward with this is central to the whole intent of the tau "experiment" itself. However, you are correct that we do need a fully specified (and not just any specification, but a stable and sustainable one) system at genesis. There are, however, two aspects to this concern: the core protocol itself (reference client) and the initial logical state encoded into the data/rules found in the genesis block.
We only intend to "prescribe" from our ivory tower the former, the protocol itself. We feel it is important that for the genesis block initial logic we do not simply dictate down some initial rules-from-on-high, but instead we hope to gather insights, suggestions, proposals, alternatives, from as broad a community involvement as we can manage to assemble at that time to hopefully reach some initial informal consensus around our initial formal consensus model.
At the beginning, it will be you, HMC (is he still involved btw? Haven't seen a single post of him since you created this thread and you seem to be running the git repo as a one-man-show these days, would be nice if he could chime in and say "Hi"!) and a handful of early users who will be busy enough trying to understand the thing and rather unlikely to have much to say about the way the original network should be bootstrapped.
Hi! I am still involved. You probably won't see me on the github (for a variety of reasons) but I regularly code up samples, examples, explanations, etc for the participants in the irc channel. Mostly, however, what I do is answer questions and resolve confusions, it seems.
The git repo is not quite as much a one-man-show as it might appear. We basically have 3 active developers, not counting myself, attempting to finish an as-close-to-ideal-as-we-can-get implementation of the core logic. We have several "draft passes" at the fundamentals of the inferencer, but are still working to finish meeting our requirements necessary to support our primary use cases.
It is sometimes a flurry of developments and sometimes almost-painfully slow going. Anyone reading this who feels that they might have something to contribute to development should feel encouraged to stop in and try to help out.
I understand that future plasticity of the protocol is important and probably one of the key strengths of Tau, but it's difficult enough to understand what is the actual plan to start with, so I (and I guess, given the level of participation so far, most people reading this thread) would be content working on the approximation / fallacy that the initial network will be a centrally designed thing so that we can spend more time understanding what will be there at launch, and less time trying to get around a non-formalized specification that feels a bit like quicksands at the moment.
Although it seems to be the "most often proposed approach" we really hope to avoid launching with a "fully centralized" genesis. Even though it seems that almost everyone involved says (jokingly? seriously? who knows..) they'd be perfectly fine with an initial rule-set along the lines of "any future rule change just needs to be signed by both Ohad and HMC" we really find this to be both quite undesirable and quite unfair both for ourselves and for our hypothetical future users.
The total opposite proposal, a system of "full anarchy" (where initially anyone may simply mutate any rule) has also been brought up a few times, but we recognize that such an approach is trivially unstable and self-defeating.
I can't say what our genesis rules will look like. I can tell you anything you'd want to know about the protocol itself, the core logic and type theory, what ultimately could/couldn't be done with the system, and any other aspect or concern leading right up *to* the moment of genesis, but "what genesis will be like" is neither something that I will speculate about, nor something worth any speculation, at least not until it is time to actually sit down and write up real (codified in the logic) proposals for genesis. That being something that I firmly believe should NOT be done by one or two people in a vacuum, anyway.
Ok, I'll probably work on that app when the core is ready.
We have a series of "proof-of-concept" tests planned for tau, which we call "litmus tests" and are designed to verify (in stages) that our construction of the system does support the intended use cases in a stable way. Many of these tests would have quite a bit of overlap with something like "git on tau" although tauchain itself is not very "git like" in many ways.
Regarding the question of how to incentivize DHT participants, I think you'd probably do yourself a great service by starting with an existing DHT network and add later a native one once other more prioritary items have been dealt with. SAFENet is nearing completion and should be live by the time Tau Chain is ready to launch. There is also Ethereum Swarm in the pipeline. That could be a good temporary solution, and it will allow Tau to ride on the coat-tails of SAFE and Ethereum. Once the Zennet side of things is live, you can create a DHT over Zennet. I think Tau Chain shouldn't try to reinvent the wheel and instead use other pateforms as much as possible to reduce the time to market. As you say, nothing is set in stone, so such decisions will be easily reversible later down the line. If you create built-ins to allow DHT-as-a-service, Blockchain-as-a-service, Storage-as-a-service, Computing-as-a-service etc, all it will take to add new services is to implement clients in Tau or bridge native clients in using the FFI, and have them register with the service manager underlying the "as-a-service" built-ins. Tau Chain can be the glue that binds existing resources on the Internet: a badly needed thing! That's also more in the spirit of the original Zennet.
It should be noted that the DHT and blockchain semantics used by tau are to be defined in the on-chain logic. In a sense, tauchain is self-describing. Only the necessary interface signatures for both the dht primitive operations and the blockchain primitive operations are specified in the core protocol, their implementations themselves are left to the on-chain logic. This precludes using "an existing DHT network" explicitly.
Further, it should be noted that we have no desire to "ride" anyone's "coat tails" anywhere. Our work is independent, should stand for itself, and should succeed or fail of its own merits.
Finally, while interoperability with other networks/services is desirable and possible under our design, this is an aspect that has to be treated with some specific care. The tauchain system itself can only operate and communicate within it's logical framework, which means that the only protocol it can actually speak is rdf. For many networks/services some extra "bridge" will be required, and such a bridge necessitates certain trade-offs with regard to the assurances and capabilities that the system provides.
Now, as for the original point of incentive, this is a bit tricky... We only care directly about incentive for the root chain, and assume any other contextual incentive would be defined contextually, of course. However, the root chain is, in a funny sort of way, "self-incentivizing by default." The root chain should never need to offer an explicit reward for resource contributions, because it's continuing operation *is* itself the reward! The continued existence and continuation of the root chain should be enough, alone, to give sufficient incentive for resource contribution to secure the continued existence of the root chain. Because the system as a whole "lives or dies" by its' root chain, and in order for any contexts to inter-operate they must do so through consensus on the root chain, it is in everyone's best interest to contribute.
I can work through a more detailed example of how this incentive model works out in practice, but this would probably be another case where the discussion would best be had in the irc.
Following the discussion in point 2, I think the only thing that would be specific about how to write or read in a context is the transport that is used to access this context. If a URL is http://, the thing (whatever it is) that handles access to that resources will have to offer a server socket, handle HTTP over that socket, and accept HTTP verbs like GET, PUT, POST, DELETE. This is more than enough to deal with the context. If the transport is something else, like for instance SQL or the file system, the commands will be different. All that should be wrapped by one more level of abstraction so that the high-level logic only need to deal with high-level objects like standard object containers (list, vector, map etc.), standard binary objects (blob) and standard function objects / lambdas.
There are actually two concerns here, interface with the system itself and interface with/between individual contexts. The interface with the system itself is defined in terms of the type theory, and has only the "lowest level" objects of dependent records of pi/sigma types. Interface with individual contexts is done in terms of an effect type system, some "built-ins" logic, and the static dht/blockchain signatures. Any other form of interface would be context specific, and defined within the logic of those contexts.
That's interesting. I'm not familiar with ML but are you saying that not only logical terms are typed? Predicates are typed too? As functions of constant return boolean value 1 maybe? And propositions.. as a 3-tuple of typed objects? And clauses / rules ... as disjunctions of propositions would be a lists of tuples maybe? And graphs an ordered conjunction of clauses.. Another list maybe?
First, here when Ohad says ML he is referring to Martin-Lof Type Theory which is more commonly abbreviated as MLTT. (ML is ambiguous as an acronym, so confusions could easily be had.)
Under a dependently typed lambda calculus (such as MLTT) there is little distinction between terms and types. Terms may be parametrized by terms or types, and types may be parametrized by terms or types. Indeed this is where the name comes from, any dependency is allowed unlike in something like haskell where terms may depend on both types or terms but types may only depend on other types, not on terms.
Propositions are not functions of boolean return, but are types which are parametrized by terms and/or types and which map to types. You can think of them more like functions which return types, not as functions that return booleans.
If it a binary tree, or a more general form of tree?
If it's a binary tree, doesn't that get in the way of code reuse?
It is a general tree. Further, the leaves of this tree are made ordinal by the cumulative universe hierarchy. This gets into some of the nitty-gritty details that Ohad was trying to avoid, but we could point you in the direction of quite a few references on the matter if you'd like. (Our "go-to starting point" lately is "Programming in Martin-Löf's Type Theory" from Chalmers.)
I may repeat myself, but I think we should focus on getting a "good enough" solution for the start, and rely on the universality of the protocol to postpone the headaches of how to converge to the ideal solution later. There are plenty of projects that deal with the issue of incentivizing peers to store data reliably over a DHT. We should start by relying on these and then work on implementing a native alternative if the quorum feels that this is a top most priority. The other advantages is that it will help Tau at the beginning to be a part of the ecosystem of already popular networks. Tau is so deeply different that there is nothing to fear and nothing to lose by cutting corners at the beginning.
Ouch, there is indeed "nothing to lose" except for the long term viability of sustainability of the system itself. If we don't take some great care "up front" then the system as a whole will tend toward trivial self-destruction. (We have quite a few thought experiments to such an effect, btw... more good fodder for discussion in the irc!)
I really don't think most early users will have the level of theoretical sophistication necessary to express themselves in Tau logic. This may happen at some point once people have caught up or the project has gained enough momentum among academic circles, and after enough efforts have been poured in creating ontologies to express more elaborate thoughts. But you shouldn't count on that at the beginning. Again, at the beginning, it will be you, HMC, and a handful of early users who will bootstrap the network, and communication will be done much more effectively over a good old forum or slate.
Quite frankly, I hope that you are actually very wrong on this particular point!
We intend to include, in the core, support for an OWL inference layer as a built-in "starting point" for hopefully *very* high level reasoning work. In fact, one of our biggest hopes is that we will be able to support, from day 0, specification of tau data and rules from a controlled natural language, such as ACE. Further, we expect that much of the earliest work on tau will be in the direction of contexts to support social, crowd-sourced models for systematically converting fully natural language knowledge and constraint into tau encoded contexts. Most of our "long term vision" surrounds this notion of users with low technical/theoretical sophistication being able to express their notions both with and to tauchain, easily and without significant specialized domain knowledge outside of a basic fundamental understanding of tau's mechanics. Further, our hope is that within "almost-no-time-at-all" tau will be able to support communication and coordination much more effectively on-chain, over itself, than on the "good old forum or slate." Indeed many of our group's intended "side projects" are along such lines. (Development tools "of tau, for tau, by tau" on chain.)
So there is nothing preventing us from already discussing what the day-0 Tau Chain will look like and creating a spec.
Only ourselves! We feel that it is much more important to focus on the protocol core and reference client, since genesis semantics "shouldn't be up to us" anyway, and any attempt to specify this logic before the core is complete is "too early." Further, we think that imposing any of our own opinions and beliefs into the conversation "before the conversation has begun" is (potentially) downright dangerous to the ultimate outcome of the project. We'll gladly discuss (to a point) some general ideas of ways that it "could work" but will not go so far as to begin to specify the genesis rules until it is actually time to do so "for real."
I hope this post has served to clear up some of your questions, and has provided a clearer picture of the design and intent of tauchain. Again I'd like to encourage you to join our irc discussions as there is really no better way to come to an understanding of what we're doing, where we're at with it, and where we intend to go.
Thank you for your interest, and I look forward to further discussion!
--HMC
