Bitcoin Forum
May 21, 2018, 11:21:57 PM *
News: Latest stable version of Bitcoin Core: 0.16.0  [Torrent]. (New!)
 
   Home   Help Search Donate Login Register  
Pages: « 1 ... 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 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 ... 157 »
  Print  
Author Topic: Tau-Chain and Agoras Official Thread: Generalized P2P Network  (Read 279966 times)
ohad
Hero Member
*****
Offline Offline

Activity: 891
Merit: 1000

http://idni.org


View Profile WWW
May 11, 2017, 06:44:37 AM
 #1801

well the old tau design (which you see in the website) is nomic-based, but not the new one (which was partly revealed here). to come up with a candidate rule, which is a single turn in nomic, is a whole mission by its own, that deserve collaboration. aside neglecting more human aspects (like the need to vote to possibly so many and so complex rules). nomic therefore cannot really scale or become decentralized, or useful in large groups.
the point is to have a decentralized ever growing knowledgebase, in a social network setting. this as for itself doesnt require a blockchain. but the next step does: to make the system itself self-defining and self-amending, collaboratively yet securely, in a decentralized fashion

What's the ETA when you get something that describes this in more detail?

unless the buyers stop me due to fear of competition or so, some in few days, some in few weeks, it seems (only seems)

Tau-Chain & Agoras
1526944917
Hero Member
*
Offline Offline

Posts: 1526944917

View Profile Personal Message (Offline)

Ignore
1526944917
Reply with quote  #2

1526944917
Report to moderator
1526944917
Hero Member
*
Offline Offline

Posts: 1526944917

View Profile Personal Message (Offline)

Ignore
1526944917
Reply with quote  #2

1526944917
Report to moderator
Advertised sites are not endorsed by the Bitcoin Forum. They may be unsafe, untrustworthy, or illegal in your jurisdiction. Advertise here.
1526944917
Hero Member
*
Offline Offline

Posts: 1526944917

View Profile Personal Message (Offline)

Ignore
1526944917
Reply with quote  #2

1526944917
Report to moderator
1526944917
Hero Member
*
Offline Offline

Posts: 1526944917

View Profile Personal Message (Offline)

Ignore
1526944917
Reply with quote  #2

1526944917
Report to moderator
FrictionlessCoin
Hero Member
*****
Offline Offline

Activity: 798
Merit: 1000



View Profile
May 11, 2017, 10:30:50 AM
 #1802

well the old tau design (which you see in the website) is nomic-based, but not the new one (which was partly revealed here). to come up with a candidate rule, which is a single turn in nomic, is a whole mission by its own, that deserve collaboration. aside neglecting more human aspects (like the need to vote to possibly so many and so complex rules). nomic therefore cannot really scale or become decentralized, or useful in large groups.
the point is to have a decentralized ever growing knowledgebase, in a social network setting. this as for itself doesnt require a blockchain. but the next step does: to make the system itself self-defining and self-amending, collaboratively yet securely, in a decentralized fashion

What's the ETA when you get something that describes this in more detail?

unless the buyers stop me due to fear of competition or so, some in few days, some in few weeks, it seems (only seems)

Well looking forward to this.  I know writing a white paper can be very challenging, but sometimes you can't be perfect.

victorserrano
Newbie
*
Offline Offline

Activity: 18
Merit: 0


View Profile
May 12, 2017, 09:39:23 AM
 #1803

Hello Ohad, What do you think of the BOScoin platform?

It is a decentralized and self-evolving blockchain, that is, it could be self-defined as TauChain. It has a network of congresses and any user can join the congress to vote and change the code or rules of the network. It also uses the web ontology language but unlike TauChain that will use RDF, BOScoin will use OWL DL since according to the white book of BOScoin the ontological language RDF does not support P-time integrity (although I do not know exactly what it means). BOScoin wants to combine the OWL language with TAL, since the latter models the programming logic. What significant differences and advantages could TauChain bring to BOScoin?

https://boscoin.io/en/home/


ohad
Hero Member
*****
Offline Offline

Activity: 891
Merit: 1000

http://idni.org


View Profile WWW
May 12, 2017, 12:14:58 PM
 #1804

Quote from: victorserrano
Hello Ohad, What do you think of the BOScoin platform?

It is a decentralized and self-evolving blockchain, that is, it could be self-defined as TauChain. It has a network of congresses and any user can join the congress to vote and change the code or rules of the network. It also uses the web ontology language but unlike TauChain that will use RDF, BOScoin will use OWL DL since according to the white book of BOScoin the ontological language RDF does not support P-time integrity (although I do not know exactly what it means). BOScoin wants to combine the OWL language with TAL, since the latter models the programming logic. What significant differences and advantages could TauChain bring to BOScoin?

https://boscoin.io/en/home/




boscoin, like tezos, broadly speaking, interested in a consensus/governance/amendment model of a currency, part of its underlying mechanics, and smart contracts. tau is about the very general concept of people forming sharing and following an idea collaboratively (and eventually doing so to tau itself). therefore unlike the other two, it doesn’t even have a coin.
not only we claim that “there is no one consensus scheme to rule them all”, we also claim that “there is no one language to rule them all”, far to mention one complexity class like P, which i can understand the rationale leading to this choice in a coin ledger setting, however i doubt whether P is enough to express self-amendment. the new tau is about human-machine-human group communication, that also lets its users to define languages and even reason over their logical properties (like completeness and consistency). the language doesn’t matter, can speak any language, as long as someone taught tau to understand it. im holding myself from pointing to more differences in order to keep some technical surprises for later.

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

Activity: 798
Merit: 1000



View Profile
May 12, 2017, 02:03:57 PM
 #1805

Quote from: victorserrano
Hello Ohad, What do you think of the BOScoin platform?

It is a decentralized and self-evolving blockchain, that is, it could be self-defined as TauChain. It has a network of congresses and any user can join the congress to vote and change the code or rules of the network. It also uses the web ontology language but unlike TauChain that will use RDF, BOScoin will use OWL DL since according to the white book of BOScoin the ontological language RDF does not support P-time integrity (although I do not know exactly what it means). BOScoin wants to combine the OWL language with TAL, since the latter models the programming logic. What significant differences and advantages could TauChain bring to BOScoin?

https://boscoin.io/en/home/




boscoin, like tezos, broadly speaking, interested in a consensus/governance/amendment model of a currency, part of its underlying mechanics, and smart contracts. tau is about the very general concept of people forming sharing and following an idea collaboratively (and eventually doing so to tau itself). therefore unlike the other two, it doesn’t even have a coin.
not only we claim that “there is no one consensus scheme to rule them all”, we also claim that “there is no one language to rule them all”, far to mention one complexity class like P, which i can understand the rationale leading to this choice in a coin ledger setting, however i doubt whether P is enough to express self-amendment. the new tau is about human-machine-human group communication, that also lets its users to define languages and even reason over their logical properties (like completeness and consistency). the language doesn’t matter, can speak any language, as long as someone taught tau to understand it. im holding myself from pointing to more differences in order to keep some technical surprises for later.

I am curious if you have any literature that discusses what you are talking about here?  More specifically this idea about human-machine-human group communication.
ohad
Hero Member
*****
Offline Offline

Activity: 891
Merit: 1000

http://idni.org


View Profile WWW
May 12, 2017, 04:24:06 PM
 #1806

Quote from: victorserrano
Hello Ohad, What do you think of the BOScoin platform?

It is a decentralized and self-evolving blockchain, that is, it could be self-defined as TauChain. It has a network of congresses and any user can join the congress to vote and change the code or rules of the network. It also uses the web ontology language but unlike TauChain that will use RDF, BOScoin will use OWL DL since according to the white book of BOScoin the ontological language RDF does not support P-time integrity (although I do not know exactly what it means). BOScoin wants to combine the OWL language with TAL, since the latter models the programming logic. What significant differences and advantages could TauChain bring to BOScoin?

https://boscoin.io/en/home/




boscoin, like tezos, broadly speaking, interested in a consensus/governance/amendment model of a currency, part of its underlying mechanics, and smart contracts. tau is about the very general concept of people forming sharing and following an idea collaboratively (and eventually doing so to tau itself). therefore unlike the other two, it doesn’t even have a coin.
not only we claim that “there is no one consensus scheme to rule them all”, we also claim that “there is no one language to rule them all”, far to mention one complexity class like P, which i can understand the rationale leading to this choice in a coin ledger setting, however i doubt whether P is enough to express self-amendment. the new tau is about human-machine-human group communication, that also lets its users to define languages and even reason over their logical properties (like completeness and consistency). the language doesn’t matter, can speak any language, as long as someone taught tau to understand it. im holding myself from pointing to more differences in order to keep some technical surprises for later.

I am curious if you have any literature that discusses what you are talking about here?  More specifically this idea about human-machine-human group communication.

let me know if you find any

Tau-Chain & Agoras
victorserrano
Newbie
*
Offline Offline

Activity: 18
Merit: 0


View Profile
May 12, 2017, 04:50:30 PM
 #1807

Hello Ohad, this is the idea I have about TauChain, correct me if I'm wrong.

TauChain is a decentralized p2p block chain network in whose block a code is stored with the operating rules of that platform. When the TauChain platform is officially released, the Genesis block will come standard without specific rules that define it and will be its first users to develop these rules. It could be said that it will be the first decentralized system of governance whose laws and rules will be marked by the consensus of the entire user community. The development of the current blockchain and its development depends on the group of programmers have designed the system, for example, Ethereum depends on its developers to evolve since it can not be modified by the consensus of other people outside the team, so they must practice Hardfork every time they want to update the system, this could be a problem since many chains of Ethereum could be left in the market, confusing the user and quoting along with the rest of chains Ethereum, an example of this would be Ethereum classic. In contrast, Tauchain will not need Hardfork to evolve as it will improve and update its code according to the consensus of all its users, which would make it a completely decentralized system. From what I understand, your work Oham and the team of the rest of the team that is designing Tauchain is not to update or fully develop the network, but to create its beginnings so that once it is released to the public, its users are those who work on it. That is, you are trying to create the intelligent Tau language and incorporate it into a chain of blocks.

Within the chain of TauChain blocks can be created centralized and decentralized applications that can be constantly updated according to the rules that have been imposed when they have been programmed. I suppose there will be applications whose development is centralized, others semi-decentralized and others whose development will be totally decentralized to TauChain.

Another feature that would make TauChain unique is the use of an intelligent language that will be able to understand and virtually express rules, processes and any arbitrary knowledge such as contracts, mathematical proofs, facts, scientific arguments and legal documents.

One of its first applications or platforms on Tauchain is Agoras whose native currency (Agora) will make up a total of 40 million. Agoras, unlike other decentralized economic markets, will be the first smart money market due to the Tau language, and will create different economic applications such as the current Augur and Golem platforms on Ethereum, but unlike these, the applications of Agoras Will benefit from the advantages of Tauchain's intelligent system (smart money).

But not only will Tauchain be used to develop a new economic system but its intelligent and decentralized block chain can be used to create new decentralized platforms based on blockchain technology that has nothing to do with the economy.

In conclusion Tauchain could be the origin of the origin of a community blockchain network.
ohad
Hero Member
*****
Offline Offline

Activity: 891
Merit: 1000

http://idni.org


View Profile WWW
May 12, 2017, 10:12:37 PM
 #1808

Hello Ohad, this is the idea I have about TauChain, correct me if I'm wrong.

TauChain is a decentralized p2p block chain network in whose block a code is stored with the operating rules of that platform. When the TauChain platform is officially released, the Genesis block will come standard without specific rules that define it and will be its first users to develop these rules. It could be said that it will be the first decentralized system of governance whose laws and rules will be marked by the consensus of the entire user community. The development of the current blockchain and its development depends on the group of programmers have designed the system, for example, Ethereum depends on its developers to evolve since it can not be modified by the consensus of other people outside the team, so they must practice Hardfork every time they want to update the system, this could be a problem since many chains of Ethereum could be left in the market, confusing the user and quoting along with the rest of chains Ethereum, an example of this would be Ethereum classic. In contrast, Tauchain will not need Hardfork to evolve as it will improve and update its code according to the consensus of all its users, which would make it a completely decentralized system. From what I understand, your work Oham and the team of the rest of the team that is designing Tauchain is not to update or fully develop the network, but to create its beginnings so that once it is released to the public, its users are those who work on it. That is, you are trying to create the intelligent Tau language and incorporate it into a chain of blocks.

Within the chain of TauChain blocks can be created centralized and decentralized applications that can be constantly updated according to the rules that have been imposed when they have been programmed. I suppose there will be applications whose development is centralized, others semi-decentralized and others whose development will be totally decentralized to TauChain.

Another feature that would make TauChain unique is the use of an intelligent language that will be able to understand and virtually express rules, processes and any arbitrary knowledge such as contracts, mathematical proofs, facts, scientific arguments and legal documents.

One of its first applications or platforms on Tauchain is Agoras whose native currency (Agora) will make up a total of 40 million. Agoras, unlike other decentralized economic markets, will be the first smart money market due to the Tau language, and will create different economic applications such as the current Augur and Golem platforms on Ethereum, but unlike these, the applications of Agoras Will benefit from the advantages of Tauchain's intelligent system (smart money).

But not only will Tauchain be used to develop a new economic system but its intelligent and decentralized block chain can be used to create new decentralized platforms based on blockchain technology that has nothing to do with the economy.

In conclusion Tauchain could be the origin of the origin of a community blockchain network.

very good. but there's quite more to it

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

Activity: 30
Merit: 0


View Profile
May 14, 2017, 03:06:11 AM
 #1809

even tezos which i thought were decent at least biz-wise, i've been notified that they copy from my writings (and even my mistakes
https://hackernoon.com/smart-contracts-turing-completeness-reality-3eb897996621
many do that, and i'll take them all to court one day, but it's the first time i saw that tezos do something like that

This is complete BS, but please take us to court and we can discuss the libelous statement you've just made.


ohad
Hero Member
*****
Offline Offline

Activity: 891
Merit: 1000

http://idni.org


View Profile WWW
May 14, 2017, 08:19:05 AM
 #1810

the long reply i promised to that tezos article. it refers only to the article. more on why i dont think tezos can work can be found on this thread not long ago.

(not the whole article is quoted below, some paragraphs are omitted for the sake of brevity)

Quote
The meltdown of “The DAO” and, more recently DDOS attacks on Ethereum have spurred a debate on the wisdom of “Turing completeness” in smart contract languages.

Tezos, a cryptographic ledger and smart contract platform offers Turing complete smart contracts in a formally specified language (with strong typing and static type checking). We seek to clarify some misconceptions about the relevance of “Turing completeness” in the context of smart contracts.

the article presents in a partial and inaccurate way the ideas i published against eth's turing completeness and lack of formal verification (beginning ~1y before the dao case, i was the first public voice and virtually the only till then, just google "tauchain turing complete" and see that others say also that tau is the only, at least months before that article). it then claims that those ideas were wrong and turing completeness is the way to go (which is a new piece of info to me, i didnt know tezos is turing complete, negative bonus points), and the way to maintain security tezos offers is again the old tau concept of static type checking (in contrast to the new tau and with other non-type-theoretic methods). in addition i refer to the (somewhat wrong) use of rice theorem i spoke a lot about (who else?). "spurred a debate" is far from describing what the sources of those ideas is.
therefore i take this late uninvited opportunity to respond.

Quote
Unfortunately, with power comes complexity. Rice’s theorem tells us that, in principle, no general procedure (human or mechanical) can decide for all programs whether they will terminate. In fact, it may not even predict any nontrivial property about their behavior.

this is somehow inaccurate and repeated along the article. the halting problem was posed and proved undecidable by turing himself. rice's theorem shows that many properties of machines can be translated to the halting problem (not so hard to see it: construct a machine that decide some nontrivial property, feed it with input from another machine, and you can determine whether the latter machine halts).

Quote
Some languages forego Turing completeness and their programs can be shown always to halt. Such is the case for the Bitcoin script for instance. A folk belief seems to be that the converse of Rice’s theorem is true. Namely, the misconception goes:
“Since the halting problem in Turing complete languages implies that we cannot predict the behavior of programs in general, then, as long as we write our programs in a language that guarantees termination, we’ll be able to predict all the interesting properties we’d like.”

This is not true, not in theory, not in practice. There are languages for which programs are guaranteed to halt for all input, but where you may not decide if any given input will cause the program to reach an error condition. (For the theoretically inclined: take for instance the language consisting of a single program f which checks if its input x is a proof of the inconsistency of ZFC. f always halt, but whether or not it ever returns “true” is undecidable in ZFC)

that's not entirely a misconception. decidability and termination go hand by hand: decidablity is the existence of a turing machine that decides the problem in finite time (not to be confused with completeness, where a complete theory can decide everything from within itself). so if type inference is guaranteed to terminate, then type inference is decidable. however that’d be a misconception indeed to try to identify decidability with termination on broader scopes.

Quote
In practice, Turing completeness is an idealization. Concretely, computers have a finite amount of memory and will only run for a finite amount of time before being turned off.

turing complete is not "real", that's right, but, the language (alongside the reasoning process) may be as abstract as well. more below.
but another point for now to be used later: the fact that machines are limited in real life, doesnt help you a single bit when it comes to undecidable problems, only worse. as an example, take hilbert’s 10th problem. given a multivarite polynomial, decide whether it has zeros over the integers. this problem is undecidable. and the fact that our machines are limited doesn't help us at all to solve it but only “makes the situation worse”.

Quote
Tezos (or Ethereum) smart contracts are bounded in time by a limit set per block and per transaction. In some trivial way, they are not quite Turing-complete. Better, since the number of steps in the execution of a contract is bounded, it is theoretically possible to predict the behavior of a given program for any possible input.

all good, but, in which sense, your (or others') type system take can take into account this boundess? even if it exists, the language typically just ignores it, so practically back to unbounded turing completeness, when trying to formally verify programs, with no information about the bounds ever propagating into the logic, hence nothing to promise the existence of a finite proof. recall that rice's theorem is not true at all when it comes to the specific machine implementation, however it still have much to say about the machine independent behavior of a program.
in other words, the mere existence of a bound external to the language, does not imply decidability of a langauge. this point is similar to, but different from, the point with hilbert’s 10th problem. these are two different issues.
what does the gas model essentially say? look at it the other way around: your contract will be forced to terminate after max known amount of steps, but, you cannot know apriori how many steps your contract is going to need! that's not avoiding the unsolvable problem, that's making it worse.

Quote
Since parsing an input takes an amount of time at least commensurate with the length of the input, the cap on the number of steps in the execution bounds the maximal size of any input that the contract may read. The following algorithm can thus decide the behavior of any contract:
for(all inputs < max size) {
   run program for max time;
   check property;
}
Of course, this algorithm is astronomically unpractical. If the input size were restricted to a measly kilobyte, there may still not be enough free energy in the universe to carry out the computation.
My point here isn’t to show that we can always prove all the true properties of time bounded smart contracts. Quite the opposite, my point is that the existence of a general algorithm and the existence of a practical algorithm are two very different things.

to the last statement, practical algorithm depends on the existence of any algorithm ofc, which cannot come unless the language is decidable.

Quote
Does such an efficient algorithm exist for Bitcoin script? The answer is no as well!

Consider the following Bitcoin script
scriptPubKey: OP_HASH256 0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef OP_EQUAL
This is a hash puzzle, as described on the bitcoin wiki. Notice that the hash I picked is clearly made up. The script clearly halts for all input, but we might be interested to know if this output is spendable. It all depends if there exists a preimage to the hash I made up, and that is absolutely unclear. We would have to brute force the hash function for billions of years to find out.

Bitcoin’s script lack of Turing completeness is not a magic bullet. It is of no help in deciding a fundamental property of this very simple script.

that'd be an innocent cheating (that partly “fixed” below). efficient and general (as below) algorithms do exist for btc scripts, yes. taking the full semantics of hash/sig and reaching a situation where its inversion is needed, is completely outside the interest of a script verifier. for all practical purposes, btc scripts can be verified very efficiently and generality.

Quote
As we’ve said before, Rice’s theorem essentially tells us that there exist programs which do terminate, and do behave as expected, but not provably so.

However, almost all correct programs of interest are going to be essentially provably correct. Moreover, the proof of their correctness will be relatively straightforward. This is especially true in the context of smart contract on cryptographic ledgers which generally implement simple and straightforward business logic (it is of course less true if you’re dealing with, say, computational algebra).

was "the dao" above "straight forward" as here?

Quote
A correctness proof might rely on admitting certain hard to prove conjectures. For instance, we may accept from heuristic arguments that hash functions are indeed hard to invert, and use it as a lemma in our proof, as is generally done in cryptography papers.

But overall, whenever a programmer writes a program, they generally keep a vague outline of a proof of correctness in their head. Sometimes that proof is incomplete or wrong — humans are fallible — but it always guides the writing. The programmer constantly reasons about he behavior of their program, to make sure it does what is intended.

this has a lot of truth. most of programs work or dont work because of "stupid reasons", not because some deep unknown math mystery. but what you explained is valid for one programmer. only then it fits all into one mind. but what if different people write different pieces of code that glue into one sw? you cannot then rely on the human knowing the proof. you need the automated (rather interactive) method, which can be done only in a decidable world.  

Quote
The efficient frontier, and the new frontier created by automated theorem proving and formal verification

Programming languages exist below an expressiveness / ease to reason about frontier.

Expressive languages make it easy to describe certain desired behavior. While, in principle, all Turing languages can express the same type of computations, in practice, it can be very hard to express certain computations if the language is inadequate. A humorous example is the Malbolge language. While Malbolge is Turing complete, it is extremely hard to write programs in this language that do what they are intended to do.

Like expressiveness, ease to reason about is not a binary variable. Turing completeness has important theoretical and practical implications for the general possibility of reasoning about a language, but as we’ve seen earlier, it does not tell the whole story.
Very expressive languages tend to be harder to reason about, while some restricted languages (such as finite state machines) can be very easy to reason about at the cost of expressiveness. There is fortunately a way to push that frontier: formal verification.

being a high-level language by no means has a anything to do with being an expressive language. that’s a horrible mis-use of the term “expressiveness” on this scope. assembly and python have same expressiveness. the former is a low-level language and the latter is a high-level.

and that’s not just a terminology issue. you claim that expressiveness has a tradeoff with ability to reason over. that’s true. but that’s true for the “real” expressiveness! not for being high/low level!

Quote
Formal verification is a rising computer science discipline which produces provably correct programs. You might think of it as creating a machine checkable proof that a program is correct, though, oftentimes, the proof itself is a program. Smart contracts have few lines of code, but a lot at stake, making them a perfect candidate for this technique.

In particular, assisted, or even automated, theorem proving lets the programmer specify the properties they want to prove and lets the computer do most of the tedious work of coming up with a formal proof of correctness. This does not affect all languages equally.

While it is true that a provably correct program is still provably correct when compiled down to some assembly, it is much harder to derive proofs from the compiled version. This is true for humans, this is true for automated theorem provers. The compilation step throws away vital information about the structure of the program.

Since Tezos started in the summer of 2014, a core tenet of the project has been that smart-contract languages are a perfect target for formal verification. We wanted a language that would play nicely with theorem provers, but also that could also be easily reasoned about on its own. This led to the following choices:

there are many formal-verifiers for C, and excellent ones. like cbmc (which you’ll find under a different yet slightly less abused buzzword: “model checking”), or astree (has to do with “abstract interepretation” and “galois connections”). of course they’re limited and not intended for others to verify my code, but for me to verify my own code. that’s a big difference when it comes to a decentralized network.  but let’s continue further before emphasizing the main point here:

Quote
We started with a formal specification of the language, to determine precisely and exactly what the program meant.

just to be clear, "what the program meant" means how to compile/interpret the program, not that it is correct. i cant see other interpretation to this sentence.

Quote
We made the language strongly typed, with algebraic datatypes and static type checking. Types are a powerful way to reason about the behavior of a program. They can ensure for instance that we do not mistakenly add apples and oranges, but they can be pushed further to enforce certain properties of the contract.
We made the language high-level. The contract that participants enter into isn’t some obfuscated assembly, but the language in which the contracts are written. This allows us to introduce useful high level primitives, such as functional maps, and functional sets. Our goal isn’t to build some arbitrary code execution engine, but an engine tailored to the needs of smart-contract writers.

good it speaks about “high level” and not “expressive” as above.
but high level has, as above, has nothing to do with essential ease to reason over. what it actually means i’ll explain at the conclusion.

Quote
All these properties facilitate proving facts about the contracts using automated theorem provers such as the Coq proof assistant, but they also make it easier to manually check the correctness of the programs.

weird. in which sense coq is auto and your approach is manual? coq is a semi-automatic typechecker as well. it typically supports undecidable theories. and for the parts that coq can be automated, i.e. type checking goes without further questions to the user, in what it is different from your proposed approach? do you propose to do all typechecks manual whatsoever?

Quote
Conclusion
Turing completeness was framed! There are programs for which properties are easy to understand and prove, and some for which they are difficult. There are programming languages which facilitate such proofs, and some which obscure them. It’s about trade-offs, not about some bright line around the halting problem.

to summarize the last quoted paragraphs,
tezos offer to do what everyone already did while knowing since the birth of computer science that it’s not achieable: to make a turing complete language that is easy to read. that human who reads the code (ok short smart contract code alright) will fully understand its behavior.
the whole offer boils to “we do a more readable language”.
yes you automatically prevent the programmer to mix apples with oranges, but that’s older than our both ages combined, in everyday programming langauges. it’s true even for assembly to some extent (and there are typed assembly languages).
excuse me but i have to dismiss the project due to boredom and lack of innovation. rooted in some good conceptions mixed with misconceptions. and also mixed with good intentions, i believe.

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

Activity: 36
Merit: 0


View Profile
May 14, 2017, 09:19:49 AM
 #1811

Everyone on this thread. I understand you want Ohad to release the whitepaper.

But coming from a tech background (utter failure, raised the money and bombed hard), to a moderately (I'd say more successful than most) business and marketing background. Particularly creating products for big brands. I think Ohad needs to build the product. I've spent the last few years of my life working with companies like Disney, Sony, Google etc. I'm not saying we need to work with the big brands but, I understand a little bit about the game and what attracts people to projects.

I must say, it is all about:
a) Product, product, product
b) Clear definition between the next guy

That's why I think we should let Ohad build the product first and release the whitepaper a little later so he can get a headstart on other people looking to either copy or capitalize on his writings. All the whitepaper will do is put him further away from the product. It may raise the price a little and get some media attention but that's so short term, what works long term is to be able to SHOW people something tangible, something that we can all fuck with and show a friend. Lets face it, a small percentage of people on this thread will fully read the white paper and a smaller amount will fully understand it. But, with product we can all get involved and it's something easier to share and explain to others.


ohad
Hero Member
*****
Offline Offline

Activity: 891
Merit: 1000

http://idni.org


View Profile WWW
May 14, 2017, 09:41:16 AM
 #1812

maybe i'll do it somewhere in the middle: release the meta-language (standalone) and first alpha (centralized) papers

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

Activity: 36
Merit: 0


View Profile
May 14, 2017, 10:17:18 AM
 #1813

I entirely agree Smaragda.  Cool

So, go for it Ohad.

Product time.
arthurb
Jr. Member
*
Offline Offline

Activity: 30
Merit: 0


View Profile
May 14, 2017, 03:15:01 PM
 #1814

the long reply i promised to that tezos

I don't find your comments particularly insightful, but whether you agree or disagree with the article is besides the point. You've made an accusation of plagiarism and threatened legal action. I'll be waiting for a retraction and apology.
ohad
Hero Member
*****
Offline Offline

Activity: 891
Merit: 1000

http://idni.org


View Profile WWW
May 14, 2017, 03:18:28 PM
 #1815

i didnt accuse you in stealing ideas but for misrepresenting my voice that you disagreed with on that article.
as i pointed out here https://bitcointalk.org/index.php?topic=950309.msg18963244#msg18963244
and on the long reply.
further i didnt even mean to threat you with legal actions. but to threat the actual (other) copiers

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

Activity: 30
Merit: 0


View Profile
May 14, 2017, 03:30:48 PM
 #1816

i didnt accuse you in stealing ideas

Quote
even tezos which i thought were decent at least biz-wise, i've been notified that they copy from my writings (and even my mistakes
https://hackernoon.com/smart-contracts-turing-completeness-reality-3eb897996621
many do that, and i'll take them all to court one day, but it's the first time i saw that tezos do something like that

Ahem.

ohad
Hero Member
*****
Offline Offline

Activity: 891
Merit: 1000

http://idni.org


View Profile WWW
May 14, 2017, 03:32:55 PM
 #1817

i didnt accuse you in stealing ideas

Quote
even tezos which i thought were decent at least biz-wise, i've been notified that they copy from my writings (and even my mistakes
https://hackernoon.com/smart-contracts-turing-completeness-reality-3eb897996621
many do that, and i'll take them all to court one day, but it's the first time i saw that tezos do something like that

Ahem.



and i clarified.
so you claim that the voice on that article was not mine? ...

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

Activity: 30
Merit: 0


View Profile
May 14, 2017, 04:29:06 PM
 #1818

i didnt accuse you in stealing ideas

Quote
even tezos which i thought were decent at least biz-wise, i've been notified that they copy from my writings (and even my mistakes
https://hackernoon.com/smart-contracts-turing-completeness-reality-3eb897996621
many do that, and i'll take them all to court one day, but it's the first time i saw that tezos do something like that

Ahem.



and i clarified.
so you claim that the voice on that article was not mine? ...

What voice? I wrote that article and I certainly didn't base it on any of your writings. I've heard of tau-chain because people have made the rapprochement with Tezos before, but that's about it.

Even the 2014 Tezos paper notes that statefulness, not Turing completeness is what makes Ethereum contract special.
ohad
Hero Member
*****
Offline Offline

Activity: 891
Merit: 1000

http://idni.org


View Profile WWW
May 14, 2017, 04:30:19 PM
 #1819

you say that turing completeness was framed. by who?

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

Activity: 30
Merit: 0


View Profile
May 14, 2017, 05:44:59 PM
 #1820

you say that turing completeness was framed. by who?

A bunch of folks as a Google Search will reveal. It's a common misconception about Rice's theorem that no programs can be analyzed.

https://www.reddit.com/r/btc/comments/4p0gq3/why_turingcomplete_smart_contracts_are_doomed/
https://steemit.com/thedao/@dana-edwards/turing-complete-smart-contracts-can-never-be-trustworthy
https://news.ycombinator.com/item?id=11941758

My turn. You said I copied your writing. Show me evidence of me copying your content or retract and apologize.
Pages: « 1 ... 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 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 ... 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!