@Ohad, I have a question. I've skimmed through the IRC logs of the last two months and found a very promising conversation between you, HMC and Stoopkid on 6 June about the maths of the new Tau. As far as I have been able to understand, HMC and Stoopkid where trying to understand how MSOL is able to verify higher order programs in spite of not being itself a full second order logic. And you were answering something about the higher order program being fully beta-reduced and encoded as a tree which apparently was supposed to turn it into a first order expression. Then the tone quickly deteriorated, and you ended up rage quitting the conversation without finishing your explanation.
As a result three questions / remarks which I found very interesting were left unanswered / undevelopped to my disappointment.
23:37 < HMC_a> so yes or no, is there a second(+) order expression which cannot be consistently proven in any mso framework? In general is full second/third order collapsible to msol, or isn't it?
I expect this one must be discussed somewhere in the works of Bruno Courcelle so you could point us to some theorem or conjecture if that can save you some time with the explanations. Don't worry about making it understandable for the mere mortals. I'm happy with an explanation that I can't fully comprehend so long as HMC and you seem to be on the same page.
22:17 < HMC_a> but maybe I'm missing some collapsability magics, somewhere, so perhaps you could give a concrete example of verification of such an example?
I concur wholeheartedly with this one. A simple example of a second or third order program in STLC+Y with limited inputs, executed against all input combinations and encoded as a tree, and then the demonstration of how msol verifies it would be hugely helpful getting some intuitive understanding of how it works. That would give us the tools to try to find a case where it doesn't work (there shouldn't be any). You can recycle that explanation for the whitepaper, so no time wasted here.
22:18 < naturalog> in bohm tree you dont have lambda terms
22:18 < naturalog> they're all reduced already
22:18 < naturalog> so the higher order rules disappear and remain only with true/false or other info
What kind of reduction are you talking about? How can the result not have lambda terms? Do you mean no lambda abstractions / bound variables? How do you guarantee that?
I understand that you probably don't want to bother making these explanations if you feel the tone of the conversation on IRC was not respectful, but please remember that IRC conversations are more or less supposed to serve as documentation and research log in the absence of actual documentation, and that they benefit the entire community, including investors and potential future devs who can help you on the code, so it would greatly help if technical questions are actually being answered.
I'm really glad to see that you, HMC and Stoopkid are trying to get back to discussing the maths, but at the same time your (as in all three of you) lack of maturity is really appalling. You are reading like an old divorced couple who hate and yet still love one another, pulling each other's leg every few sentences, and lacing otherwise perfectly factual questions and answers with half concealed vitriol and sarcasm. Rage quitting and yet coming back for more. Really not constructive. A giant waste of time and intelligence.
If you really care as much about Tau / Autonomic as you all pretend, you should be able to keep your egos in check and apply a minimum of self-control to make sure that conversation doesn't turn into a nasty troll fest before it has the time to reach its conclusion. After all, if both of your are confident about your maths, it really shouldn't be a problem to set the record straight. And if you are not, it's fine (who am I to judge?), but then stop acting as if you are Field medalists and be humble and honest about what you don't know.