Quote from: klosure on February 20, 2017, 06:59:13 PM

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?

i saw it on their website. by generic knowledge i basically refer to the expressiveness of their language.
they do require you to write code. code can be seen as a proved statement, which is fine, but is up to the programmer to prove in many cases, however it requires more than that. this has structural implications on how you can say what you have to say. it's a point i'm frequently strugging to explain, but let's try the following. when we write a contract, or a book, we mean that all sentences written there are true. we implicitly mean that the reader should take the *conjunction* of all sentences/clauses/paragraphs. i refer to this as the "conjunctive nature" of how we express ourselves. proofs and programs, on the other hand, are of compositional nature. think i'd like to express an in idea for you in writing, so i write a paragraph with many holes such that you cannot understand a thing out of it, and then i give you words and half-sentences to substitute on those holes, many of such sets of substitutions, and you'll have to read that first paragraph again and again but with different substitutions in the hole places. you'd hate that. but machines love that. i believe that we should stick to our conjunctive nature, and let machines translate it by themselves into a compositional nature.
what this practically means is,
specification is also of conjunctive nature. typically, you want a program that do/satisfy "this AND that AND that". the order doesn't matter. unlike the curry-howard approach in old tau (similar also to prolog), on the new tau executing the program does not mean "executing the spec/logic", namely the operations taken have nothing to do with the reasoning process, and we don't invoke curry-howard correspondence at all. the logic is about the program, is not the program itself. and has a conjunctive nature, especially when it comes to large number of participants, each stating their opinion.
there's much more to say, and i'll say slowly.

Quote from: klosure on February 20, 2017, 06:59:13 PM

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.

indeed we don't follow the coq way in many senses. not to say anything bad about coq, the contrary. it's just for slightly different purposes.
yes Miller had a lot to do with "proof of execution", economically hashing the execution tree for selected datatypes. Zooko is a very knowledgable guy as well.

Quote from: klosure on February 20, 2017, 07:19:45 PM

Quote from: ohad on February 20, 2017, 05:52:50 PM

how do you expect people to form well-formed proposals, that actually express what they meant and so on?
do you expect this to be an individual process for experts?
on the new tau we consider this a collaborative process for non-experts, the process of forming a proposal, aside the process of accepting it.

I think it's wishful thinking to imagine that non-experts will be able to amend the protocol or understand deeply what they are voting for. Tezos's solution apparently is to allow people who don't understand what they are asked to vote for to delegate their votes to someone they believe knows better and shares their perspective. Not a bad idea. At best, you could have experts rephrasing the decision in simpler terms in plain english, but then you would still need to trust that they are not misrepresenting the problem or showing a bias, and you would still need people to really try to understand what they say at a logic level which isn't a given, and then there is the laziness. As pointed in the interview, the DAO was a good example of how in practice, most people won't really bother voting.

think of the "facebook with controlled english" metaphore.

Quote from: klosure on February 20, 2017, 07:19:45 PM

Quote from: ohad on February 20, 2017, 05:52:50 PM

a smaller point would be regarding votes. once you take a close look, you don't need them anymore

Would that be a solipsistic look or a totalitarian look or an omniscient look Wink

?

by no means the system will tell people what to think. but votes isn't necessarily the best way. your opinion can be extracted from all your other opinions that you stated, or that others stated and you agreed/disagreed with. can you imagine people voting for proposals all day, rather state their worldview "once" and forever?

(they may change their mind too). that's in very very short