Bitcoin Forum
July 21, 2018, 08:15:36 AM *
News: Latest stable version of Bitcoin Core: 0.16.1  [Torrent]. (New!)
 
   Home   Help Search Donate Login Register  
Pages: « 1 ... 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 [74] 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 ... 159 »
  Print  
Author Topic: Tau-Chain and Agoras Official Thread: Generalized P2P Network  (Read 280668 times)
infovortice2013
Legendary
*
Offline Offline

Activity: 1176
Merit: 1000



View Profile WWW
November 05, 2016, 02:18:20 PM
 #1461

this project its a ICO, so until the product is ready investors usually cant trade nothing, its a good thing stay in bittrex but is evident than buying support is hard to find because already havent product to promote or use. but if you wanna cash out from ico cose you want btc for whatever reason ey its no sobad maybe btc price has doubled since the ico was.

Dont mix dev in trading questions man have nothing to do its a free market. and dev not need go to sell in bittrex, proyect is already well funded in $$$

sure i trust ohad can finish it at his own, if not can hire devs he needs.

yeah all of us want it developed faster XD i not going to lie. must go and buy some patience.
1532160936
Hero Member
*
Offline Offline

Posts: 1532160936

View Profile Personal Message (Offline)

Ignore
1532160936
Reply with quote  #2

1532160936
Report to moderator
1532160936
Hero Member
*
Offline Offline

Posts: 1532160936

View Profile Personal Message (Offline)

Ignore
1532160936
Reply with quote  #2

1532160936
Report to moderator
fair bitcoin games | pvp - pve - solo pve games | faucet |
Free satoshi code btcoon500
Advertised sites are not endorsed by the Bitcoin Forum. They may be unsafe, untrustworthy, or illegal in your jurisdiction. Advertise here.
1532160936
Hero Member
*
Offline Offline

Posts: 1532160936

View Profile Personal Message (Offline)

Ignore
1532160936
Reply with quote  #2

1532160936
Report to moderator
1532160936
Hero Member
*
Offline Offline

Posts: 1532160936

View Profile Personal Message (Offline)

Ignore
1532160936
Reply with quote  #2

1532160936
Report to moderator
1532160936
Hero Member
*
Offline Offline

Posts: 1532160936

View Profile Personal Message (Offline)

Ignore
1532160936
Reply with quote  #2

1532160936
Report to moderator
ICOcountdown.com
Hero Member
*****
Offline Offline

Activity: 714
Merit: 500


View Profile WWW
November 08, 2016, 10:39:14 PM
 #1462

https://www.youtube.com/watch?v=KRxjowVPChs

Interview with Ohad. Smiley

freequant
Hero Member
*****
Offline Offline

Activity: 770
Merit: 500


View Profile
November 08, 2016, 11:41:22 PM
 #1463

Golem ICO starting on 11 Nov. Golem endeavors to create a distributed computing platform similar to Zennet on Ethereum. Any opinion on the relative worth of this project?
ohad
Hero Member
*****
Offline Offline

Activity: 893
Merit: 1000

http://idni.org


View Profile WWW
November 09, 2016, 12:54:46 AM
 #1464

Golem ICO starting on 11 Nov. Golem endeavors to create a distributed computing platform similar to Zennet on Ethereum. Any opinion on the relative worth of this project?

to be honest i dont think that ethereum will hold for too long due to its turing complete nature. indeed golem evolved into something that looks like specific cuts from zennet

Tau-Chain & Agoras
freequant
Hero Member
*****
Offline Offline

Activity: 770
Merit: 500


View Profile
November 09, 2016, 10:29:29 PM
 #1465

indeed golem evolved into something that looks like specific cuts from zennet
Is this an endorsement?
ohad
Hero Member
*****
Offline Offline

Activity: 893
Merit: 1000

http://idni.org


View Profile WWW
November 09, 2016, 11:18:21 PM
 #1466

indeed golem evolved into something that looks like specific cuts from zennet
Is this an endorsement?

they still have major design issues as nicely pointed eg here http://elastic-project.com/comparison_with_other_solutions

Tau-Chain & Agoras
dmitryshech
Member
**
Offline Offline

Activity: 115
Merit: 10


View Profile
November 13, 2016, 10:29:06 PM
 #1467

I am invested in this project and I believe that indeed it can make a significant change. I am relatively new to this and I never was involved in discussions on this tread or on the whole forum in general but there is a point that I want to deliver here.

Ohad very talented and brilliant tech guy, I am sure he knows what he does and he is very dedicated to the project but at this point it looks like he is struggling to  tell the right story to the masses and as a result this project is the most underestimated on crypto community today, Golem it's a very good proof to that point.

to be honest i dont think that ethereum will hold for too long due to its turing complete nature. indeed golem evolved into something that looks like specific cuts from zennet

That is probably true and they indeed may still have "major design issues" an so on... The fact is: THEY COLLECTED 8,2 MILLIONS OF DOLLARS IN 20 MINUTES

Which means, from a regular, non tech investor point of view:

1. the Golem's idea is clearer, they marketing telling the story in the right language that investors understand
2. the branding and website design is much better
3. there is a serious team working on the project

My question to Ohad is:

Is there already, or you are looking for some talented marketing/brending/design people to join the project, some one who can brake down the whole major value points of this project and create out of them very good, understandable and persuading story that speaks directly to the target audience.

Thank you
ohad
Hero Member
*****
Offline Offline

Activity: 893
Merit: 1000

http://idni.org


View Profile WWW
November 13, 2016, 11:19:50 PM
 #1468

to be honest i dont think that ethereum will hold for too long due to its turing complete nature. indeed golem evolved into something that looks like specific cuts from zennet

That is probably true and they indeed may still have "major design issues" an so on... The fact is: THEY COLLECTED 8,2 MILLIONS OF DOLLARS IN 20 MINUTES

note that it might be due to money that comes in only in order to show big investments (and then roll that money out and in again from a back door). i'm not saying golem did such, but important to bear in mind that it's possible, and tbh i got this "advice" from ethereum's presale architects.

My question to Ohad is:

Is there already, or you are looking for some talented marketing/brending/design people to join the project, some one who can brake down the whole major value points of this project and create out of them very good, understandable and persuading story that speaks directly to the target audience.

Thank you

there is, and this will be reflected in the new website (which is waiting for me for quite long time already but i'm so busy on other things)

Tau-Chain & Agoras
John_Paul
Sr. Member
****
Offline Offline

Activity: 270
Merit: 250


View Profile
November 15, 2016, 12:56:15 AM
 #1469

to be honest i dont think that ethereum will hold for too long due to its turing complete nature. indeed golem evolved into something that looks like specific cuts from zennet

Do you think the projects like Augur, First Blood and Golem can be easily moved to Tau-Chain if Ethereum is not working as expected in the future?
ohad
Hero Member
*****
Offline Offline

Activity: 893
Merit: 1000

http://idni.org


View Profile WWW
November 15, 2016, 01:36:14 AM
 #1470

to be honest i dont think that ethereum will hold for too long due to its turing complete nature. indeed golem evolved into something that looks like specific cuts from zennet

Do you think the projects like Augur, First Blood and Golem can be easily moved to Tau-Chain if Ethereum is not working as expected in the future?

technically yes but they will have so much competition since tau will enable features that were not possible before (two examples: decidability and self-definition).

Tau-Chain & Agoras
johny08
Legendary
*
Offline Offline

Activity: 1043
Merit: 1000


View Profile
November 16, 2016, 03:18:31 PM
 #1471

Golem ICO starting on 11 Nov. Golem endeavors to create a distributed computing platform similar to Zennet on Ethereum. Any opinion on the relative worth of this project?

to be honest i dont think that ethereum will hold for too long due to its turing complete nature. indeed golem evolved into something that looks like specific cuts from zennet

you are saying, you are working with turing complete nature systems too. so its not really a counterargument.

transcripts of the interviews would be nice, because of the complexity. the topic itself is complex. sometimes i cant break it down.

ohad
Hero Member
*****
Offline Offline

Activity: 893
Merit: 1000

http://idni.org


View Profile WWW
November 16, 2016, 05:58:37 PM
 #1472

Golem ICO starting on 11 Nov. Golem endeavors to create a distributed computing platform similar to Zennet on Ethereum. Any opinion on the relative worth of this project?

to be honest i dont think that ethereum will hold for too long due to its turing complete nature. indeed golem evolved into something that looks like specific cuts from zennet

you are saying, you are working with turing complete nature systems too. so its not really a counterargument.

tau is not turing complete.

Tau-Chain & Agoras
LiskEnterprise
Sr. Member
****
Offline Offline

Activity: 268
Merit: 250


View Profile
November 19, 2016, 03:11:45 PM
 #1473

Golem ICO starting on 11 Nov. Golem endeavors to create a distributed computing platform similar to Zennet on Ethereum. Any opinion on the relative worth of this project?

to be honest i dont think that ethereum will hold for too long due to its turing complete nature. indeed golem evolved into something that looks like specific cuts from zennet

you are saying, you are working with turing complete nature systems too. so its not really a counterargument.

tau is not turing complete.


Tau is a language right?

So why not run it on Safe Network.

After maid safe opens up why even have a blockchain?

http://heatledger.com LIVE ICO 3.0 GENERATION CRYPTO WITH COMPANY STOCK IPO OPTIONS
ohad
Hero Member
*****
Offline Offline

Activity: 893
Merit: 1000

http://idni.org


View Profile WWW
November 19, 2016, 05:00:06 PM
 #1474

Golem ICO starting on 11 Nov. Golem endeavors to create a distributed computing platform similar to Zennet on Ethereum. Any opinion on the relative worth of this project?

to be honest i dont think that ethereum will hold for too long due to its turing complete nature. indeed golem evolved into something that looks like specific cuts from zennet

you are saying, you are working with turing complete nature systems too. so its not really a counterargument.

tau is not turing complete.


Tau is a language right?

So why not run it on Safe Network.

After maid safe opens up why even have a blockchain?

there's a big difference between maidsafe and tau. it'll be much clearer on the upcoming paper

Tau-Chain & Agoras
VintageBazaar
Sr. Member
****
Offline Offline

Activity: 566
Merit: 257


Born in Crypto late 2013.


View Profile WWW
November 20, 2016, 08:02:17 AM
 #1475


Very good interview,would be really great if the "common crypto guy" could understand it,  this must also be the reason for the bump start in volume, now Agoras on the 3rd row on Bittrex.

 

                                                                           ▄▄▄ ▄▄▄▄▄▄▄▄▄▄▄▄▄▄▄▄▄▄▄▄▄▄
                                                                           ███ ███████████████████████
                                                                           ███    ███
                                                                           ███    ███
                                                                           ███    ███
       █       ███      ███   ▄████████▄  █▄         ▄█ █████████ █▄       ███    ███   ▄▄███████▄▄   ████████▄   ▄▄██████▄▄
      ███      ███      ███  ████▀▀▀▀██▀  ███▄     ▄███ ███▀▀▀▀▀▀ ███▄     ███    ███  █████▀▀▀█████  ███▀▀▀████ ████▀▀▀▀██▀
     █████     ███      ███ ███▀          █████▄ ▄█████ ███       █████▄   ███    ███ ████       ████ ███    ███ ███▄
    ███ ███    ███      ███ ███   ▄▄▄▄▄▄▄ █████████████ ███▄▄▄▄   ███████▄ ███    ███ ███         ███ ███▄▄▄████  █████▄▄
   ███   ███   ███      ███ ███    ██████ ███ ▀███▀ ███ ███████   ███ ▀███████    ███ ███         ███ █████████▀    ▀▀█████▄
  ███     ███  ███▄    ▄███ ███▄      ███ ███   ▀   ███ ███       ███   ▀█████    ███ ████       ████ ███  ███          ▀███
 ███       ███  ███▄▄▄▄███   ████▄▄▄▄████ ███       ███ ███▄▄▄▄▄▄ ███     ▀███    ███  █████▄▄▄█████  ███   ███  ▄██▄▄▄▄████
███         ███  ▀██████▀     ▀█████████▀ ███       ███ █████████ ███       ▀█    ███   ▀▀███████▀▀   ███    ███ ▀▀███████▀
         BATTLE FOR DOMINANCE
 
|
 
 
|
 

                   ▄▄████
              ▄▄████████▌
         ▄▄█████████▀███
    ▄▄██████████▀▀ ▄███▌
▄████████████▀▀  ▄█████
▀▀▀███████▀   ▄███████▌
      ██    ▄█████████
       █  ▄██████████▌
       █  ███████████
       █ ██▀ ▀██████▌
       ██▀     ▀████
                 ▀█▌
TELEGRAM
 

█▄▄              █▄▄
█████▄▄         ██████▄▄
████████       ████████ █
████████ ██   ████████ ██
████████ ███ ████████ ███
████████ ████ ██████ ████
████████ █████ ████ █████
████████ ▀█████ ██ ██████
████████    ▀▀██  ███████
▀███████         ▀███████
   ▀▀███            ▀▀███
       ▀                ▀
UPDATES
 

  ███▄▄                  ▄▄███
 ███████████ ▄████▄ ███████████
▐█████▀▀████ ██  ██ █████▀▀████▌
████▀▀  ▀▀██   ▄██▀ ██▀▀█  █▀▀██
████      ██   ██   ██  █▀▀█  ██
██████  ████        █████  █████
████████████   ██   ████████████
████████                ████████
███████                  ███████
▐█████                    █████▌
 ▀███                      ████
  ▀▀                        ▀▀
TESTERS
 

█▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀█
█                    ▄▄▄▄  █
█                    ████  █
█        ▄▄▄▄        ████  █
█        ████        ████  █
█        ████        ████  █
█        ████  ████  ████  █
█  ████  ████  ████  ████  █
█  ████  ████  ████  ████  █
█  ████  ████  ████  ████  █
█                          █
▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀
DATABITS
LiskEnterprise
Sr. Member
****
Offline Offline

Activity: 268
Merit: 250


View Profile
November 21, 2016, 10:36:26 AM
 #1476

Golem ICO starting on 11 Nov. Golem endeavors to create a distributed computing platform similar to Zennet on Ethereum. Any opinion on the relative worth of this project?

to be honest i dont think that ethereum will hold for too long due to its turing complete nature. indeed golem evolved into something that looks like specific cuts from zennet

you are saying, you are working with turing complete nature systems too. so its not really a counterargument.

tau is not turing complete.


Tau is a language right?

So why not run it on Safe Network.

After maid safe opens up why even have a blockchain?

there's a big difference between maidsafe and tau. it'll be much clearer on the upcoming paper


Can you provide your description of SAFE?

Is it not simply a protocol that eliminates servers and farms and thus provides a platform written in Rust to provide true decentralization? Then other apps, languages platforms can be written on-top of it but have the benefit of NO SERVERS.

There is actually no blockchain.

Tau needs a blockchain?




http://heatledger.com LIVE ICO 3.0 GENERATION CRYPTO WITH COMPANY STOCK IPO OPTIONS
ICOcountdown.com
Hero Member
*****
Offline Offline

Activity: 714
Merit: 500


View Profile WWW
November 21, 2016, 10:59:00 AM
 #1477

Golem ICO starting on 11 Nov. Golem endeavors to create a distributed computing platform similar to Zennet on Ethereum. Any opinion on the relative worth of this project?

to be honest i dont think that ethereum will hold for too long due to its turing complete nature. indeed golem evolved into something that looks like specific cuts from zennet

you are saying, you are working with turing complete nature systems too. so its not really a counterargument.

tau is not turing complete.


Tau is a language right?

So why not run it on Safe Network.

After maid safe opens up why even have a blockchain?

there's a big difference between maidsafe and tau. it'll be much clearer on the upcoming paper


Can you provide your description of SAFE?

Is it not simply a protocol that eliminates servers and farms and thus provides a platform written in Rust to provide true decentralization? Then other apps, languages platforms can be written on-top of it but have the benefit of NO SERVERS.

There is actually no blockchain.

Tau needs a blockchain?






Blockchain creates immutability of the network itself and a public record Smiley

ohad
Hero Member
*****
Offline Offline

Activity: 893
Merit: 1000

http://idni.org


View Profile WWW
November 21, 2016, 11:34:03 AM
 #1478

Can you provide your description of SAFE?

Is it not simply a protocol that eliminates servers and farms and thus provides a platform written in Rust to provide true decentralization? Then other apps, languages platforms can be written on-top of it but have the benefit of NO SERVERS.

There is actually no blockchain.

Tau needs a blockchain?

assume we build tau on safe and after some time we want to change safe's protocol itself (cause we found a bug or simply cause we have a better one) -- that wouldn't be possible, as safe isn't self-defining. that'd be one example. and yes tau needs a blockchain to contain the definition of the protocol at any point of time

Tau-Chain & Agoras
klosure
Jr. Member
*
Offline Offline

Activity: 50
Merit: 0


View Profile
November 22, 2016, 11:52:34 AM
 #1479

Catching up with latest developments. I've read some of the chat logs and the heated exchange between Ohad and HMC.

There are good arguments on both sides. HMC is right that MLTT + TFPL is a more conservative choice since it's already in use in a flurry of theorem provers and formal verification frameworks and languages. He is also right that MSOL's limitations wrt to arithmetic *could* (theoretically but no example is known) turn out to be problematic to express some categories of computations although it's unclear if that would really be a problem for practical use of Tau. Ohad is right that the TFPL constraints and the non-axiomatic LEM make MLTT + TFPL difficult to program intuitively, and somewhat amputate expressiveness in a way that's difficult to fathom and (seem) undecidable. Both approaches have shortcomings and advantages, and it's an excellent thing that both are being researched so that the project won't be stuck in a rut should one of the paradigms turn out to be unsuitable.

Now, where I'm really puzzled is that this difference of views has led to a complete breakdown of the project team in spite of the fact no party has been able to properly back their claims. There are good arguments on both sides but the so called "critical flaws" pointed by both sides are yet to be proven. Indeed MSOL over trees limitations wrt to arithmetic could be problematic, but is it a real problem? Modern computers are using bounded arithmetic operations over 32 or 64 bit registers, and can all be emulated with basic bit-wise logic operations, in a way which can be entirely flattened / unrolled and require no loop, and can be broken down into several rounds to allow execution over multiple blocks / cycles like it was planned to do with the original Tau design to recover turing completeness. If unbounded iteration can be recovered, why would arbitrary precision arithmetic be unrecoverable when the very thing to be recovered in both case is exactly the same: unbounded-ness? Now, wrt to the claim that type checking as used in MLTT+TFPL is undecidable making it very awkward to create proofs, it's also rather unsubstanciated: it is really undecidable? Without proof, the argument is moot. And even if it really was, does it really make it so awkward to create proofs in practice? Examples would be helpful. Surely the fact it's being used in Idris and Agda should hint to the fact it is at least somewhat usable.

It seems to me that both parties have good arguments, and that at the same time both also jumped the gun and decided that they were right and the other wrong based on incomplete premises propped up by ego matters. What's wrong with you guys? Whatever happened to "this too is why we need Tau"?. How can you promote the use of logic as the central tenet of Tau and yet fail to abide to it at the first occasion where a difference of views arise?

The most puzzling is that the debate has been exclusively centered around the artificially constrained question of who is right, and who is wrong (as if it was an axiom that one had to be right and the other wrong and only one form of calculus could possibly express Tau, nevermind the Curry-Howard isomorphism), all the while ignoring completely the fact that it's entirely possible for both views to coexist happily within the project. Tau is a language, based on RDF, and meant to come with a formally defined grammar and set of ontologies. As HMC has stated earlier in this thread, even OWL-DL can be recovered over Tau which means that, since both are expressed as RDF graphs, OWL-DL can be  transformed in valid Tau code by mapping and graph transforms. Regardless of whether the Tau client uses MLTT+TFPL or MSOL over trees under the hood, it will still have to support OWL-DL and programs written in the latter and that are not undecidable should work. I take OWL-DL as an example, but Tau is a superset of OWL-DL, and everything in this super-set should work equally well on any suitable logic.

The crux of the problem is that nobody knows exactly what is the spec of Tau. We know that Tau, as a language, is a superset of other languages we know it will have to support to be useful at all, like OWL-DL. But we don't quite know where exactly is its boundary. Is that a fundamental property of Tau to have limited recursion and no axiomatic law of the excluded middle? HMC will tell you it is, but not because it was the requirement or something inherently desirable, but because shoehorning Tau into MLTT+TFPL implies that Tau should have these properties. Same thing on the other side. Ohad will tell you that it should be a fundamental property of Tau to have free recursion and the law of the excluded middle but bounded arithmetic. Obviously, if everyone who comes with a new calculus gets to decide what Tau is so that it works with it, we are going to go round in circles forever. Tau shouldn't be what possible underlying forms of logic imply it should be.Tau should be that and only that which is required to express the family of programs that are both decidable and able to complete within bounded space (memory) and time on modern hardware regardless of whether doing so implies unrolling loops or emulating multiplications. Since "modern hardware" is a moving target, programs should be shipped with the size of the dimensions of the bounding box they are guaranteed to run in, together with other proofs on their properties, and should be able to run on any Tau client using any form of suitable logic. With a properly specified Tau language, you could have some Tau clients using MSOL over trees (assuming its suitable) with others using MLTT+TFPL (assuming its suitable), all capable to communicate over the tau-chain and crunch away happily. If that's not the case we are doing something very wrong, and falling for the classic mistake of retrofitting the requirements to fit the model, instead of creating the model based on requirements.

Of course this is easier said than done. As the debate between Ohad and HMC have illustrated, there are multiple ways that infinity can creep in, and different forms of logic enforce decidability by bounding calculus along different axis: recursion, or arithmetic. For a spec to be truly generic, it should include both a high level spec for developers (the language) which should be independent of the underlying logic, and a lower level spec with basic mechanisms to handle multiple forms of calculus which would include a form of generic continuation allowing the underlying logic to create deferred payloads that, stringed together, would allow to recover turing completeness. The underlying logic / implementation would know what to do when it compiles the code and how to package computation so that it runs in bounded time and space intrinsically, while allowing unbounded computation extrinsically with the blockchain used as the one and only carrier for infinity.

@HMC and @ohad: can we bury the hatchet and go back to the drawing board so that Tau will no more be bound to a single form of calculus? With such a model, both MLTT+TFPL and MSOL over trees can be implemented in parallel and trialed by fire. Tau would also become more future proof. After all, who knows: maybe a few years down the line, a new breakthrough in computer science will give rise to yet another form of calculus that could turn out to be even better. That we be too bad if Tau is stuck in a too specific model and fails to evolve.

We are all in the same boat, hoping to have a way to unleash logic upon the world and enable a new era of global rationality. It would be a pity if that grand vision didn't come true due to petty cat fights between project founders. You are two smart guys, and I know you know what really matters, and that this doesn't include petty ego matters.
ohad
Hero Member
*****
Offline Offline

Activity: 893
Merit: 1000

http://idni.org


View Profile WWW
November 22, 2016, 01:26:45 PM
 #1480

thanks, some more and less important notes:

Catching up with latest developments. I've read some of the chat logs and the heated exchange between Ohad and HMC.

There are good arguments on both sides. HMC is right that MLTT + TFPL is a more conservative choice since it's already in use in a flurry of theorem provers and formal verification frameworks and languages.

i wouldn't necessarily agree with that since there are also many msol-based model checkers (mona, libvata etc) aside many other model checkers for subsets of msol (LTL, CTL, mu-calculus [which is equi-expressive with msol in some cases, and less expressive in other] etc). cf https://en.wikipedia.org/wiki/List_of_model_checking_tools

He is also right that MSOL's limitations wrt to arithmetic *could* (theoretically but no example is known) turn out to be problematic to express some categories of computations although it's unclear if that would really be a problem for practical use of Tau.

should distinguish between what we can compute and what we can assert. indeed those two are same under dependent types. but for our msol setting, indeed msol cannot express parts of arithmetic, but is just the requirement language. the programming language itself is stlc+y (equivalently finitary pcf) and can express more than all multivariate polynomials over finite sets (for infinite base types *without recursion*  cf https://pdfs.semanticscholar.org/a2ef/cfb7401b3e87ed3e9574183f47e75ae58617.pdf )
hmc's main objection is, as he said, the "lack of general product in stlc+y". but product is just currying.. stlc supports products just fine.

Ohad is right that the TFPL constraints and the non-axiomatic LEM make MLTT + TFPL difficult to program intuitively, and somewhat amputate expressiveness in a way that's difficult to fathom and (seem) undecidable. Both approaches have shortcomings and advantages, and it's an excellent thing that both are being researched so that the project won't be stuck in a rut should one of the paradigms turn out to be unsuitable.

Now, where I'm really puzzled is that this difference of views has led to a complete breakdown of the project team in spite of the fact no party has been able to properly back their claims. There are good arguments on both sides but the so called "critical flaws" pointed by both sides are yet to be proven. Indeed MSOL over trees limitations wrt to arithmetic could be problematic, but is it a real problem? Modern computers are using bounded arithmetic operations over 32 or 64 bit registers, and can all be emulated with basic bit-wise logic operations, in a way which can be entirely flattened / unrolled and require no loop, and can be broken down into several rounds to allow execution over multiple blocks / cycles like it was planned to do with the original Tau design to recover turing completeness. If unbounded iteration can be recovered, why would arbitrary precision arithmetic be unrecoverable when the very thing to be recovered in both case is exactly the same: unbounded-ness? Now, wrt to the claim that type checking as used in MLTT+TFPL is undecidable making it very awkward to create proofs, it's also rather unsubstanciated: it is really undecidable? Without proof, the argument is moot. And even if it really was, does it really make it so awkward to create proofs in practice? Examples would be helpful. Surely the fact it's being used in Idris and Agda should hint to the fact it is at least somewhat usable.

LEM is not so bad, the problem with mltt is undecidability. btw even System F has undecidable typecheck as mentioned eg here http://cs.stackexchange.com/questions/12691/what-makes-type-inference-for-dependent-types-undecidable
how can one have a sound nomic game without decidability? and that's the "critical flaw" with mltt.
proofs done with mltt are very helpful, since the language is consistent. once something is proved, we can rely on it to be true. but not every truth can be proved (or derived) in an undecidable system.

It seems to me that both parties have good arguments, and that at the same time both also jumped the gun and decided that they were right and the other wrong based on incomplete premises propped up by ego matters. What's wrong with you guys? Whatever happened to "this too is why we need Tau"?. How can you promote the use of logic as the central tenet of Tau and yet fail to abide to it at the first occasion where a difference of views arise?

The most puzzling is that the debate has been exclusively centered around the artificially constrained question of who is right, and who is wrong (as if it was an axiom that one had to be right and the other wrong and only one form of calculus could possibly express Tau, forget Curry-Howard isomorphism), all the while ignoring completely the fact that it's entirely possible for both views to coexist happily within the project. Tau is a language, based on RDF, and meant to come with a formally defined grammar and set of ontologies. As HMC has stated earlier in this thread, even OWL-DL can be recovered over Tau which means that, since both are expressed as RDF graphs, OWL-DL can be  transformed in valid Tau code by mapping and graph transforms. Regardless of whether the Tau client uses MLTT+TFPL or MSOL over trees under the hood, it will still have to support OWL-DL and programs written in the latter and that are not undecidable should work. I take OWL-DL as an example, but Tau is a superset of OWL-DL, and everything in this super-set should work equally well on any suitable logic.

by your latter argument we could have any turing complete language and restrict it over time to decidable fragments. but: how is this going to happen? i mean, how are we doing to have collaborative development without decidability? participants raise rules for vote, but as long as we cannot understand what proposals really mean (namely the implications between them, their consequences, the rules they contradict etc), we might avoid the consensus we're looking for. under undecidable yet consistent logic, you can give me proofs for your claims about your code, but decidability is required for me to ask my questions about your code.

The crux of the problem is that nobody knows exactly what is the spec of Tau.
i'm fixing this situation nowadays, writing a new and much better whitepaper

We know that Tau, as a language, is a superset of other languages we know it will have to support to be useful at all, like OWL-DL. But we don't quite know where exactly is its boundary. Is that a fundamental property of Tau to have limited recursion and no axiomatic law of the excluded middle? HMC will tell you it is, but not because it was the requirement or something inherently desirable, but because shoehorning Tau into MLTT+TFPL implies that Tau should have these properties. Same thing on the other side. Ohad will tell you that it should be a fundamental property of Tau to have free recursion and the law of the excluded middle but bounded arithmetic. Obviously, if everyone who comes with a new calculus gets to decide what Tau is so that it works with it, we are going to go round in circles forever. Tau shouldn't be what possible underlying forms of logic imply it should be.Tau should be that and only that which is required to express the family of programs that are both decidable and able to complete within bounded space (memory) and time on modern hardware regardless of whether doing so implies unrolling loops or emulating multiplications. Since "modern hardware" is a moving target, programs should be shipped with the size of the dimensions of the bounding box they are guaranteed to run in, together with other proofs on their properties, and should be able to run on any Tau client using any form of suitable logic. With a properly specified Tau language, you could have some Tau clients using MSOL over trees (assuming its suitable) with others using MLTT+TFPL (assuming its suitable), all capable to communicate over the tau-chain and crunch away happily. If that's not the case we are doing something very wrong, and falling for the classic mistake of retrofitting the requirements to fit the model, instead of creating the model based on requirements.

indeed the design i'm laying now will support many future logics (not only msol/mltt!)

Of course this is easier said than done. As the debate between Ohad and HMC have illustrated, there are multiple ways that infinity can creep in, and different forms of logic enforce decidability by bounding calculus along different axis: recursion, or arithmetic. For a spec to be truly generic, it should include both a high level spec for developers (the language) which should be independent of the underlying logic, and a lower level spec with basic mechanisms to handle multiple forms of calculus which would include a form of generic continuation allowing the underlying logic to create deferred payloads that, stringed together, would allow to recover turing completeness. The underlying logic / implementation would know what to do when it compiles the code and how to package computation so that it runs in bounded time and space intrinsically, while allowing unbounded computation extrinsically with the blockchain used as the one and only carrier for infinity.

@HMC and @ohad: can we bury the hatchet and go back to the drawing board so that Tau will no more be bound to a single form of calculus? With such a model, both MLTT+TFPL and MSOL over trees can be implemented in parallel and trialed by fire. Tau would also become more future proof. After all, who knows: maybe a few years down the line, a new breakthrough in computer science will give rise to yet another form of calculus that could turn out to be even better. That we be too bad if Tau is stuck in a too specific model and fails to evolve.

as above, i'm all for multilogic, and i even have a plan

Tau-Chain & Agoras
Pages: « 1 ... 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 [74] 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 ... 159 »
  Print  
 
Jump to:  

Sponsored by , a Bitcoin-accepting VPN.
Powered by MySQL Powered by PHP Powered by SMF 1.1.19 | SMF © 2006-2009, Simple Machines Valid XHTML 1.0! Valid CSS!