I have a few questions:

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

Supporting network features etc. is done via builtins, which is also a common mechanism among RDF reasoners. See for example

http://www.w3.org/2000/10/swap/doc/CwmBuiltins- Where can I find a Tau code example that emulates simple procedural behavior like a loop for instance?

Let me use the cwm 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/H2gqLUzC- Will the Tau node to be a full fledged RDF triple store and SPARQL end-point?

Except I won't promise now we'll use exact SPARQL syntax, then sure. Tau can be equivalently described as a decentralized triplestore with dependent types.

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

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

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

On the other hand, since the logic is decidable, the provable statements are exactly all correct statements and vice versa. Since every program has some runtime complexity, it is apriorily possible to give a proof for a runtime of any program.

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.

- Where can I find more (code / documents) about the JIT compilation of the Tau language?

This is exactly what I work on these days, so I'll have to finish first.

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

Please let me know if I missed something or if other questions arise.