Quote from: ohad on February 20, 2017, 04:57:03 PM

It might be the only thing out there that is close to tau.

Well, now there is also Autonomic

Quote from: ohad on February 20, 2017, 04:57:03 PM

that said, there's still a big gap.

I agree. Although there is quite a bit of overlap on the fundamentals, Tezos seems to be specifically aiming at protocol governance, whereas Tau is both much more general in scope and closer to the metal due to the versatility of its RDF syntax which gives it the ability to blend naturally with semantic structure of which it is only a flavor. I think we can probably learn a lot from the launch of Tezos, their approach, their mistakes, and how things pan out with the nomic game.

Quote from: ohad on February 20, 2017, 04:57:03 PM

i'd ask two things before decidability: expressibility,

I asked that already

Quote from: ohad on February 20, 2017, 04:57:03 PM

and which parts of the system are amendable (is it the whole code no matter what?).

In the EpiCenter interview, he talks about layers, of which only the topmost layer that contains functional rules about the way the blockchain is working and the business logic would be self-amending, which includes consensus rules and voting. Based on that, I think all of the lower level stuff like network communication, overlay network management, DHT etc are hard coded and evolve following a regular software life cycle. This is actually made more explicit later in the interview where Arthur Breitman explains that only changes that involve governance issues are really controversial and subject to on-chain consensus, whereas more technical issues such as bug fixes are following the normal software life cycle and adopted following the normal soft/hard fork rules as people update their clients.

Quote from: ohad on February 20, 2017, 05:45:27 PM

1. need to understand what they mean by "ledger" and in what it's different than "generic knowledge"

probably ledger = blockchain, generic knowledge = whatever state the blockchain is used to maintain?
Can you provide the context?

Quote from: ohad on February 20, 2017, 05:45:27 PM

2. ocaml impl?! ... the easy but eventually-useless way?

He mentioned in the interview that he was inspired by Coq for the formal verification. Coq is written in OCaml so going with OCaml would probably have saved quite a bit of time. I can't find back the detailed team page of Tezos, but if I remember well there were some people from Inria, so that would also explain why they went for OCaml.

Just noticed that Andrew Miller is an advisor of the project. Wasn't he also following Tau? And there is Zooko too! What a small world. I wonder if HMC knows the tezos guys.