Bitcoin Forum
May 28, 2018, 03:59:38 AM *
News: Latest stable version of Bitcoin Core: 0.16.0  [Torrent]. (New!)
 
   Home   Help Search Donate Login Register  
Pages: « 1 ... 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 125 ... 157 »
  Print  
Author Topic: Tau-Chain and Agoras Official Thread: Generalized P2P Network  (Read 280054 times)
klosure
Jr. Member
*
Offline Offline

Activity: 50
Merit: 0


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

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.
Advertised sites are not endorsed by the Bitcoin Forum. They may be unsafe, untrustworthy, or illegal in your jurisdiction. Advertise here.
1527479978
Hero Member
*
Offline Offline

Posts: 1527479978

View Profile Personal Message (Offline)

Ignore
1527479978
Reply with quote  #2

1527479978
Report to moderator
1527479978
Hero Member
*
Offline Offline

Posts: 1527479978

View Profile Personal Message (Offline)

Ignore
1527479978
Reply with quote  #2

1527479978
Report to moderator
1527479978
Hero Member
*
Offline Offline

Posts: 1527479978

View Profile Personal Message (Offline)

Ignore
1527479978
Reply with quote  #2

1527479978
Report to moderator
ohad
Hero Member
*****
Offline Offline

Activity: 892
Merit: 1000

http://idni.org


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

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
AEA
Jr. Member
*
Offline Offline

Activity: 36
Merit: 0


View Profile
November 28, 2016, 11:06:36 PM
 #1483

Sounds amazing, looking forward to further updates Ohad.
cvrizzos
Newbie
*
Offline Offline

Activity: 26
Merit: 0


View Profile WWW
December 01, 2016, 03:36:04 PM
 #1484

Dr. Ohad hi, great project.

1. Is there a chronogram or timeline for this project? when will it be finished more or less?
2. Where should we safely store IDNI Agoras (AGRS) tokens bought at bittrex exchange?

Thanks in advance,

http://www.blockitalia.com/
m4nki
Hero Member
*****
Offline Offline

Activity: 784
Merit: 500



View Profile
December 01, 2016, 03:42:09 PM
 #1485

Dr. Ohad hi, great project.

1. Is there a chronogram or timeline for this project? when will it be finished more or less?
2. Where should we safely store IDNI Agoras (AGRS) tokens bought at bittrex exchange?

Thanks in advance,


1. It is done when it's done - I think a rough estimate for Tau to reach Genesis would be summer/fall 2017.
2. You can store AGRS safely by transfering them to any Bitcoin address that you have the private key to. Later you can import them into the omniwallet.org once the swap to the coin on top of Tau-Chain is being done.

ICOcountdown.com
Hero Member
*****
Offline Offline

Activity: 714
Merit: 500


View Profile WWW
December 01, 2016, 03:49:16 PM
 #1486

Dr. Ohad hi, great project.

1. Is there a chronogram or timeline for this project? when will it be finished more or less?
2. Where should we safely store IDNI Agoras (AGRS) tokens bought at bittrex exchange?

Thanks in advance,


1. It is done when it's done - I think a rough estimate would be summer/fall 2017.
2. You can store AGRS safely by transfering them to any Bitcoin address that you have the private key to. Later you can import them into the omniwallet.org once the swap to the coin on top of Tau-Chain is being done.

https://www.omniwallet.org/

You can use this wallet to store at Agoras tokens. Smiley

ohad
Hero Member
*****
Offline Offline

Activity: 892
Merit: 1000

http://idni.org


View Profile WWW
December 01, 2016, 05:20:22 PM
 #1487

good answers. and i'm not a Dr. Wink

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

Activity: 892
Merit: 1000

http://idni.org


View Profile WWW
December 02, 2016, 11:30:36 PM
 #1488

Omni's decentralized exchange begins to function https://blog.omni.foundation/2016/12/01/omniwallet-updates-omnidex-trading-interface-launched/
of course our tokens are traded there as well
(i wrote to them regarding the old tokens displayed there)

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

Activity: 292
Merit: 250


View Profile
December 03, 2016, 08:45:51 PM
 #1489

I'm so excited about this project. Just wanted to bump it.
logictense
Hero Member
*****
Offline Offline

Activity: 812
Merit: 500


View Profile WWW
December 03, 2016, 08:53:51 PM
 #1490

I been using the wallpaper from the OP on my site quite a while ago. Could be found in google image search, but in the OP its cut to ugliness. OP is cutter.

ohad
Hero Member
*****
Offline Offline

Activity: 892
Merit: 1000

http://idni.org


View Profile WWW
December 03, 2016, 09:28:07 PM
 #1491

I been using the wallpaper from the OP on my site quite a while ago. Could be found in google image search, but in the OP its cut to ugliness. OP is cutter.

it's a real photo btw. a microscoping scan of human neurons

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

Activity: 812
Merit: 500


View Profile WWW
December 04, 2016, 09:24:57 PM
 #1492

I been using the wallpaper from the OP on my site quite a while ago. Could be found in google image search, but in the OP its cut to ugliness. OP is cutter.

it's a real photo btw. a microscoping scan of human neurons

This is non-related to what I said. This photo has been dashing crypto OPs for quite a while. Internet is bigger than google image, it has more similar images. But cutter put up this one.

ICOcountdown.com
Hero Member
*****
Offline Offline

Activity: 714
Merit: 500


View Profile WWW
December 05, 2016, 10:38:37 PM
 #1493

I been using the wallpaper from the OP on my site quite a while ago. Could be found in google image search, but in the OP its cut to ugliness. OP is cutter.

it's a real photo btw. a microscoping scan of human neurons

This is non-related to what I said. This photo has been dashing crypto OPs for quite a while. Internet is bigger than google image, it has more similar images. But cutter put up this one.

It is in the vain of open source, this is also an open source image. I do like the graphic design behind it.

herkuljee
Jr. Member
*
Offline Offline

Activity: 34
Merit: 0


View Profile
December 08, 2016, 11:02:01 AM
 #1494

Someone dumped possession. Someone got cheap coins.
infovortice2013
Legendary
*
Offline Offline

Activity: 1176
Merit: 1000



View Profile WWW
December 08, 2016, 02:46:25 PM
 #1495

Huge crash price in bittrex, 3btc dump ,, time to add buy support !
skrtel37
Sr. Member
****
Offline Offline

Activity: 473
Merit: 250



View Profile
December 09, 2016, 02:58:38 PM
 #1496

The thing that strikes me the most about this project is that its a "One man show".
Its not surprising that this project runs for about 2.5 years now (counting Zenet era)
In crypto time is of the essence, especially now when Golem is making such big noises....I strongly recommend
to approach other members to the team....

ImI
Legendary
*
Offline Offline

Activity: 1848
Merit: 1008



View Profile
December 09, 2016, 03:06:22 PM
 #1497


As much as i agree with adding other members to the team, i disagree on another point: please don't compare this project with Golem. Golem is a joke compared to this. And not even a functional joke as they plan to have their final version years from now.
ICOcountdown.com
Hero Member
*****
Offline Offline

Activity: 714
Merit: 500


View Profile WWW
December 09, 2016, 03:09:53 PM
 #1498

Adding more team members is an issue, because:

1.) It's going to be extremely find the same level of programmers as Ohad.

2.) There is a possibility they could deviate from the original vision.

ohad
Hero Member
*****
Offline Offline

Activity: 892
Merit: 1000

http://idni.org


View Profile WWW
December 09, 2016, 03:11:56 PM
 #1499

i'm certain that with the new upcoming whitepaper it'll be much easier to find collaborators. And there are more reasons, one of them is the planned alpha version (to be described in the whitepaper)

Tau-Chain & Agoras
SEOcrypto
Member
**
Offline Offline

Activity: 114
Merit: 10


View Profile
December 09, 2016, 05:39:13 PM
 #1500

i'm certain that with the new upcoming whitepaper it'll be much easier to find collaborators. And there are more reasons, one of them is the planned alpha version (to be described in the whitepaper)


BOOM!

Very excited to read the new whitepaper Ohad.
Pages: « 1 ... 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 125 ... 157 »
  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!