Quote from: lexxus on April 21, 2016, 02:10:59 PM

Quote from: ohad on April 21, 2016, 01:50:04 PM

Quote from: lexxus on April 21, 2016, 01:49:06 PM

Why was Martin-Lof Type Theory was chosen? Why not something more common such as first order predicate logic?

because we want consistent decidability, together with maximum computability

is lack of decidability a serious issue? afaik decidability will just allow tau to reject formulas which we know in advance are not correct theorems. so it saves miners from attempting to prove such theorems, wasting computational resources.

sorry for lame questions, I really don't remember much from my cs classes. i need to read something to brush up the topic and better understand tau. may be you could advise something to read. thanks in advance.

pls cf http://www.idni.org/blog/generalized-blockchain