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.