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*


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

It's possible; we can only make a comparison based on those aspects of the design that have been publicly disclosed, so we can only really address the question of MSOL vs. MLTT. Both HMC and Ohad claim to know the answers here, but their answers are in contradiction with each other. Previously I had thought I was able to demonstrate the insufficiency of MSOL but upon closer analysis I realized that my proofs were based on flawed assumptions and misinterpretations. Since coming to this realization, have taken a step back from "pushing the MLTT agenda", and now my goal is simply to play the role of a neutral 3rd party and analyze the validity of these claims, along with carrying out some further research into the strengths and weaknesses of various other logical systems that could potentially be used (mainly just standard systems discussed frequently in academic literature on formal logic, as these have the most metatheoretic results available to aid in the comparisons, and are the most likely systems to be brought up as an actual candidate logic as MSOL and MLTT have). I'll share my results with the community as I go along, on the AutoNomic wiki, though I will warn ahead of time that the explanations will still be very technically involved; it's simply a complex subject.


I'm guessing you mean HMC, myself and the AutoNomic project? Anyway, we were all originally working with Ohad but we split for various reasons, one major factor being Ohad's choice to change the planned logical framework from MLTT to MSOL. The history's all in the thread and the IRC logs, and I don't feel like dragging it up. Tau continued as same name, new design. AutoNomic continued as same design, new name. Adding this question of which logical framework to use has indeed "stalled" at least our side of the project as it's now added the goal of rigorously sorting out the differences between... nearly every standard logical framework presented in academic literature on the subject or in modern use in automated theorem proving and proof-checking, though we are still developing the MLTT-based client in parallel to this for concrete experimentation (and because until our research indicates a flaw in this choice we'll continue under the operating assumption that it will still eventually be the chosen framework). I can't speak to what's going on on the Tau side of things though (from what I understand it's not even publicly disclosed).

Edit to fix grammar mistakes.

As Obama once put it: "Yes we can."

I've been discussing with Nilli on the zennet IRC channel and there's been a couple points I thought could use some elaboration. I was a bit confused myself as to how a reaction from Coke and Disney would lead to a rise in value of the coins. Most of my confusion was due to me thinking of these coins as if they were any other crypto-currency, rather than as the artwork / collector's items that they really are (see the previous posts by HunterMinerCrafter and Nilli discussing the similarity to WotC/Wizards of the Coast and MtG/Magic the Gathering). 


 < stoopkid> nilli: you've said that in the event that coke/disney react to the coins (which i think is probably very likely to happen depending on how this goes), that the value of the coke/disney coins would rise; could you elaborate on how coke/disney's reaction would cause a rise in value?
< stoopkid> HMC_Alph: maybe you have some thoughts to that as well?
< HMC_Alph> https://en.wikipedia.org/wiki/Succ%C3%A8s_de_scandale



< nilli> As art controversy is the best thing for it
< nilli> as coins having the buzz  all that matter


And it's really just as simple as that! If the remainder of the coins are burned after distribution is finished, the coins will be collector's items simply due to their scarcity, but in the event that Coke and Disney decide to react against the coins, then the coins will have far more desirability for collectors: from those just looking for more Coke/Disney memorabilia to those looking to have their hands on a piece of one of the great controversies of our time (not to mention that in the event that the coins do rise in value, people would seek to collect them just for that reason).

Btw Nilli thanks for mentioning Tau!  

Hi Nili I'm looking forward to seeing how this turns out! Here's my wallet address:

13WEZ2RSTAC2dZwY5s36LssdiTmxoLb7gX