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?
the proofs being automatic comes from the theory being decidable, and the manual requirements in idris/agda stem exactly from the undecidability problem. and indeed tau must be decidable as it must be a sound nomic game: the network should know when someone obey or break a rule, with no false positives or false negatives. under idris/agda, due to the undecidability, you can obey the rules yet not necessarily be able to prove it.
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.
msol is substantially better as it is decidable (which also imples automatic proofs).
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.
complexity of proof is pretty much the same in both systems (i.e. unlimited complexity). it doesn't mean that even easy tasks will take very long time, it only means that it's able to solve even very hard problems. in addition, k-exptime for example is just a worst case bound. it is commonly said (e.g. by Ong) that this worst case should be achieved quite rarely, and not in common human programs.