- Do you have a specification (ontology, BNF grammar, spec document...) of the Tau language as it is now and/or as it is supposed to become once all the networking and crypto features are built in?
The syntax of the language itself is not new. The RDF family is basically all syntax-sugaring to NQuads
http://www.w3.org/TR/n-quads/ so all RDF languages can be converted to NQuads, while plenty of converters out there. Current tau's code can read NQuads, JSON-LD, and (yet partial) Notation3.
I wasn't asking about RDF triples and NQuads: these are just a representation format. What I am asking is the specification of the Tau language itself. OWL2 for instance is the RDF implementation of a logic language called SROIQ(D) formally specified
here that is a subset of description logic and its derivation as RDF based ontology is specified in great details
here.
We know from the whitepaper that Tau is borrowing to constructive / intuitionist logic. But is it a subset, a variation, or does it implement the full logic? Is there a whitepaper or document covering the formalism? Is there a document that describes the ontology including the core logic and library of built-ins related properties?
Is Tau entirely structured around CWM? What about the builtins that are not already implemented by CWM? For instance DHT related features, RNG etc. Will you contribute them to the original CWM? Are you going to fork CWM to extend it? Or does CWM come with a way to register new builtins and if it does is it statical (compile time) or dynamic (runtime)?
- Where can I find a Tau code example that emulates simple procedural behavior like a loop for instance?
Let me use the cwm's builtins I just linked to demonstrate printing numbers from 1 to 10:
1 log:outputString 1.
{ ?x log:outputString ?x. (1 ?x) math:sum ?y. ?y math:lessThan 11 } => { ?y log:outputString ?y }.
see
http://pastebin.com/H2gqLUzCYou are using the W3C swap/math and swap/log ontologies.
Are they a subset of the Tau ontology?
Again, that would need to be clarified. What IS valid Tau and what is not?
- How do you plan to make the transition from knowledge (decision of spawning a new socket for instance) to action (making a system call to create a new socket): will each i/o module poll the knowledge base periodically for relevant action? Will you place control points at key steps of the inference process to intercept propositions with a known action semantic and take action?
- Will input from i/o module trigger asynchronous reasonning or will it just add new propositions in the knowledge base for some synchronous process to reason with at next iteration?
At the syntax level, IO is just another builtin predicate, like { ?z a tau:tcpEndpoint } => { ?y tau:tcpConnect ?z }. At the typesystem level, we of course have Effect types/Monads
https://en.wikipedia.org/wiki/Monad_(functional_programming)
The reasoning flow does not change at all due to IO (in general), but types originated from IO are tagged as effect types and of course aren't treated as "pure truth". A good reference is how Idris use side effects
http://eb.host.cs.st-andrews.ac.uk/drafts/eff-tutorial.pdfIf I understand correctly your reply I/O originated events and data are being incorporated as new facts that will be (lazy-)evaluated / stated next time the reasoner does a resolution that needs i/o related facts, which in other words means synchronous i/o. I can see how this is going to add a lot of latency, but let me read that Idris paper first and I'll get back with more questions
- Is the interface between the knowledge base and the system level functionalities already developed or specified? Where can I find further details?
Apologies but I didn't really understand the question.
You gave this example above: "{ ?z a tau:tcpEndpoint } => { ?y tau:tcpConnect ?z }".
Are the built-ins behind tau:tcpEndpoint and tau:tcpConnect already developed or specified in a document?
What will be all the built-ins introduced by Tau?
- How can Tau guarantee that it can determine the upper bound of when a program can halt in less time than it would take to run the program? What if the program is already the shortest possible program to solve the problem it represents? At most I could imagine how code analysis could help determining a big-o estimate of the program complexity but then that won't help much to make sure that the program can run within the time boundaries of a given blockhain block as was suggested in the cointelegraph interview.
This goes right back to decidability, and to the point that one shouldn't expect the autoprover to prove all math by itself instantly.
Let me quote HMC's reply to the question "How does it compare to Ethereum" in the
interview on CoinTelegraph To contrast, Tau is a decidable complete logic, per block, with Turing completeness recovered by the iteration of multiple blocks. This means that we cannot compute any computable thing in one block, but we can know exactly how much resource expenditure a block will require to verify. We can still compute any computable thing; it may just require structuring the execution to run over the span of multiple blocks. Because of this, Tau resources do not need to be backed directly by a token, and resource exchange can be negotiated by the users as they see fit.
In the context of the comparition with Ethereum, what I understand HMC to be saying is that the question of the maximum runtime of a contract is decidable which allows to break down the contract in execution segments and schedule them over multiple blocks. Hence my question. If the only thing that is decidable for
any program (you don't control what contract creators put in a contrat) is the fact that the program will stop, this does absolutely nothing to make it anywhere near practical. If the program takes 5 years to stop, we aren't any better off than if it didn't stop at all.
So if I understand correctly, what HMC says above would work only for these contracts that were shipped together with a proof already written explicitely by the contract developer that establishes in polynomial time that the program will stop because the developer went through the deliberate design decision of making his program do everything in small chopped batches with yielding and continuations all over the place. Is that the spirit? And to ensure that every contract on the chain are following this paradigm, the contracts would need to come with the proof for the transaction to be validated and added to the blockchain? And do you also ship a proof that the proof indeed runs in polynomial time? And so on
?
Any example of a chopped contract?
Assume I write a tau or idris program that halts on the first zero of Riemann's Zeta which is not on the critical line. Of course, no one expect the prover to determine quickly if this program ever halt. If I knew how to do that magic, I'd already take $6M by solving the 6 math open problems of Clay institute
That's the point. So Tau will need to rely on a very self-constrained ultra-modular programming paradigm so that it is possible to prove that every chunk of code is both space and time bounded regardless of its input, while making sure that the proof itself doesn't become more complex than the chunk of code it vouches for...
I'm really curious how that will work in practice. A piece of code that demonstrates this would be more than welcome.
So assume I wrote some simpler code with runtime complexity that I know how to compute and prove, then I can specify my proof or parts of it, and let the prover finish the missing details.
Tau, the first Proof-of-PhD smart contract system
- Are there archives of IRC discussions / forum discussions / email discussions etc that can help understanding decisions made around the design?
I don't think there's anything one can easily track. ~10MB of text won't help anyone. So for now one can only ask and get answers, and with time we'll document everything.
I don't mind finding my way in a 10MB dump. I don't want to waste your time answering questions if the answers are already there somewhere.
Please let me know if I missed something or if other questions arise.
Proposed that nicely, how can I refuse? Here are a few more questions:
- Do you have specs about what exactly Agora is going to be. I mean other than the
story of Bob and Alice . What kind of assets will Agora allow to trade? Will it features a full fledged distributed exchange like Ripple? Will it support other market paradigms like auctions or prediction markets?
- Have you started working on Agora?
- How long do you estimate you will need to complete Agora?
- Tau ETA?
- Agora ETA?
Thanks for your questions, they raise important clarifications:
1. The OWL family is indeed a widely used ontology and known to suffer from logical complexities. Our goal is to implement RDFS (which is a relatively low level at this scope), and above it implement our type system (which probably amounts to adding predicates part-of and is-type-of, a good ref is ceur-ws.org/Vol-354/p63.pdf), and to recover OWL2 over those primitives.
I do not claim that any OWL ontology would be interpreted on tau just as any other OWL reasoner, and I do not promise any "easy migration" of existing code, as long as it is beyond just facts (i.e. without vars or rules).
So what I can tell now about tau's lang is:
a. Syntax is RDF family.
b. RDFS builtins will be supported as-is.
c. OWL will be supported as well but might not keep its common semantics' subtelties, as they change from reasoner to reasoner.
d. The rdf:Type predicate will be interpreted in a Martin-Lof dependent-type framework, as well as typechecking.
e. The language will also have Auth types for proof of execution (as in lambda-auth) and Effect types for IO.
f. The reasoner will be shipped with some builtins, this touches your next question and I'll emphasize on this in a moment.
2. The logic itself can describe everything that is computable. In other words, "all math that matters". It is so strong that it is considered as a new foundation of mathematics in general, see for example HoTT (Homotopy Type Theory). A great feature in Martin-Lof type theory is that you cannot even express a contradiction (like you can't even express Russel's paradox), therefore you never inconsistent.
3. Tau is not structured upon CWM at all. We do use Euler and Yieldprolog as references for inference and Idris/Agda as reference for typesystem, but not CWM. Moreover, I'm not aware of open-source stand-alone performance-oriented C++ reasoners out there that support N3Logic. We write everything from scratch, and in fact we already finished writing the part convering reasoning over triples. From here (except some more parsing features) is it all only features that RDF reasoners haven't met yet, at least not directly (like euler.yap jitting indirectly over swipl), to my knowledge.
4. What is valid Tau and what not is still early to answer. We will have to finish developing the language before we can say firmly "this is it".
5. To write "good" tau code one would definitely have to give a very good thinking, like any other construction. I do not claim that every first grader would write decentralized application over tau in natural language. But tau lets you focus on the logic and meaning of what you say, and help you express things unambiguously. Even if this will turn down to be more complex than say Python (which is of course a matter of taste), there are two important point to take into account:
a. Tau can have more frontends. The "real" interface is nothing but quads. Any sugaring over them can be de-sugared and fed to tau.
b. The more important point is code reuse, and to picture how programming would actually take place over tau. Say you want to write some complex program, and begin to break it up to functions and structures. Say for example that one required structure is red-black tree and one required function is balancing the tree. What you'd do nowadays is not reinvent the wheel but google this and find some code snippets for reuse. Those snippets may or may not fit your needs, and you still have to adapt them (if not reimplement them) to fit your code.
On the other hand, given tau, you can formalize only the requirements from the structure and the functions, and from here you have three options: either that code already exists in tau's records (might even be that your formal reqs themselves already exist) and you can find code that provably meet your needs, or, you can offer a reward to anyone that provable meets your requirements, or, you can write the code yourself, but this time the reasoner can give you a great help since it can prove you're correct or wrong in many cases. At the end, you end up with code that you can trust even more than after QA, since you have a mathematical proof that it meets its requirements.
6. It is worth mentioning that we intent to postpone to post-genesis everything that can be postponed to post-genesis. The a-f points I mentioned above are essential at-genesis, together with more features of course. Even the JIT is needed in order to specify the order of execution (possibly to future compilers) so client will be able to agree upon proof of execution. At this theme, all we do is give a reference, usable, and good enough client. Of course other implementations of the tau protocol are possible, just like there are many different bitcoin clients.
This might also shed some light on the common wondering "it must take years to build that monster". We indeed tend to pick the shortest path, and we believe it is shorter than estimated at first sight.
7. The IRC channel has become "home" for several friends and contain many personal and off-topic conversations. This is why I never published the logs in public. Nevertheless, you can simply join the channel and see right there how to get the logs right away.
8. I don't have specs for tau or agoras more than already published. Things are fluid during dev, ofc, and we better finish the client before we can give exact directions how to use it or what would be the features. Pretty much the same for ETA. I can throw numbers into air while apriori every number would be wrong. I can tell that 6 months till tau's genesis sounds horribly pessimistic for me, and another 6m months for agoras sounds strongly pessimistic. Sorry for being vague, but think of it for a second, and see that any other answer of mine would be a lie, and all I can do is give you the most truthful answers I have myself.
9. Have a look at
http://www.cs.ru.nl/~freek/100 of course the syntax is terrible, and this, too, is why we build tau (HMC: apologies for using your catchphrase).
10. " If the only thing that is decidable for any program (you don't control what contract creators put in a contrat) is the fact that the program will stop, this does absolutely nothing to make it anywhere near practical. If the program takes 5 years to stop, we aren't any better off than if it didn't stop at all." -- No, *everything* that can be expressed on the language is decidable! You can prove *all* *correct* theorems, and you can't even express their negation (i.e. expressing a contradiction).
I have to go now and I might add some more later. Will be happy to come back and see more questions