Yes, but if a malicious actor attempts to add a rule to the system which, within the context of the system, can only be determined valid after an inordinate period of time, wouldn't this be a problem for a MSOL based Tau? It would be, for all intents and purposes, be undecidable, correct?
i dont understand your example. please explain
An undecidable system, such as Idris/Agra has false negatives (a valid program is not accepted), but not false positives (an invalid program is accepted), correct?
yes, in consistent system such as idris/agda, once you have proof for something, then it's true. but if you don't have a proof, it doesn't mean it's false, under undecidable system
So, both systems, for all intents and purposes, have a false negative problem. When using Idris/Agra and the user inputs a program that is undecidable, the user is just asked to clarify. Similarly, it would seem, if after a certain period of processing, validity can't be determined by MSOL based Tau, then it would also need to ask the user to clarify, or reject the rule outright.
i cant see why msol would have a false negative problem?