Quote from: dmitryshech on August 16, 2017, 08:46:10 PM

I have no idea what MLTT or MSOL is... I can only imagine the levels of ego between people with so high level of proficiency in the field though. If at some point you guys instead of sticking with the academic literature until your research indicates a flaw in this choice, you will try to unite again and work on it together it will make all the community extremely happy and I am sure will contribute much better to the project.
UNITED WE STRONG
Just MHO

I'm not really sure what you mean wrt "instead of sticking with the academic literature" but I'm willing to work with anybody to either sort out the metatheoretic details or experiment with (open source, publicly disclosed) candidate implementations. The more the merrier. MLTT is simply the candidate the AutoNomic team is currently experimenting with, as it's unfinished business from HMC's original Tau plan. We don't yet have a metatheoretic proof of its insufficiency, so I don't see a reason for us to stop this experiment already in progress. If Ohad wants me to check out his new Tau plans, I'll check them out and give my honest attempt to understand and reach a conclusion, but I kind of guess that AutoNomic is at least one of the reasons that Tau has resorted to non-disclosure.

*shrug*

Quote from: Rider311 on August 17, 2017, 12:11:53 AM

Me neither. I still find it rather entertaining though. They make seemingly good points but Ohad does a good job defending himself. It's all above my head but I can get a general idea what's going on (I think).

Would someone point my towards the auto nomic thread?

We don't have a thread here, just the freenode channel #AutoNomic.