I don't know if I'm talking to anybody at this point, but the discussion with HMC and Ohad brings up the following questions:

1. Ohad seems to think that all proofs must be automatic for Tau to prevent malicious actors from attacking Tau. Couldn't the rules of the P2P nodes just require a proof of certain properties to be handed along with the rules for them to be acceptable? Be solvable in a certain amount of cycles using a given Resoner?

A general proof system that can solve all proofs automatically and quickly seems like a tall order. I mean without including the whole distributed computing P2P part of it, such a system would seem to be a major advance over what we have currently with Idris, coq and others.

Yes, the alternatives described would also work with a Turing-complete language, as well, but so what if it did? If using MLTT or MSOL isn't substantially better than a Turing-complete language, then a Turing complete language should be used.

2. Just because MSOL can be solved automatically, this doesn't mean it can be done quickly enough to be useful in Tau, isn't it? I mean that if it takes an exponential amount of time to automatically solve a question proposed in MSOL (and it seems from what I'm read that it is N-EXPTIME), then it might as well be true that some expressions aren't solvable in MSOL, right? And if that is the case, you have the very same problems of MLTT.