3 ms·

No need to forgive. You're not wrong nor naive. I'd pin the difference as one of personal risk tolerances. I have much less than you, that's all. Right now Soli

by buckie 9y ago

No need to forgive. You're not wrong nor naive. I'd pin the difference as one of personal risk tolerances. I have much less than you, that's all. Right now Solidity is the only choice of public smart contracts. All I meant before was that this is an impressive project and to be careful. > But, after all, a dark horse 20 year old college dropout spearheaded the development of Ethereum, and the technology now secures nearly 20B worth of value. This is a really common trope in finance -- the trader/quant/manager/pm who thinks that he's god's gift to earth because he made so much money (and a system that made even more). I'm not saying that's what's going on in Ethereum, far from it, just that people who make a lot of money tend to think they are worth that amount of money (usually they are just fortunate) and that using monetary value as the sole justification for one's actions is (generally) wrong. While I disagree that Eth is actually valued at $20B -- if you can't get even a fraction of the $20B out of the market then it's not worth $20B in value... I bet the buy side of the Eth market supports around $100M-$300M max -- that's neither here nor there. The Ethereum ecosystem is, invariant on the value it represents, truly impressive and Vitalik's work is amazing especially given his experience level prior to it. I wouldn't say that the EVM is well designed in the slightest but the rest of the system is. It's closer to a 80's era CPU than a modern VM. I get why it looks like it does -- taking the bitcoin bytecode and extending it as little as needed -- but I disagree with the approach at a technical level. VM's are supposed to do more (e.g. handle dispatch and library loading) and to not support that means one must implement it in the language (like an ASM compiler does) which in a blockchain context consumes the limited gas you have. > I hold an optimistic view that, as formal verification techniques for smart contracts get fleshed out and easier to use 100% Agreed, though I don't think Solidity will have it anytime soon (3-5 year min for whole program verification that experts can use, I know some of the people working on it). The path the solidity FV people are following is a long, hard research path (close to what they did for the seL4 microkernel). Moreover, I know a ton about this because I built the first whole program formal verification system (compiler + DSL) for any smart contract language[1]. I built it for Pact, the language we[2] built to address the problems we saw with Ethereum's approach in enterprise contexts, that's FOSS but currently only available for on-chain use on our private platform. It wholly fixes the "immutable code" problem[3] via cryptocharters -- think of them as a module (smart contract) that have native support for both decentralized and centralized governance mechanisms for updating contracts and migrating the data they store. There's a bunch more stuff that Pact gets right, but that's what the papers are for describing. Keep in mind that formal verification isn't the "end all be all" for program safety. While it massively advances the state of the art in that regard you need more than just FV because FV still requires human effort (just vastly less/safer than regular/auditing testing). It's just that FV is SO damn rare that most people, including myself until last year, (a) have no idea what it looks like and (b) have no idea what to use it for. People seem to think that an FV-capable language will solve all of their problems. No, it won't. How many people going to become experts in SMT/Coq/Isabell just to write a safe smart contract? They, but Coq especially, make Haskell (which already scares people off) look like a cuddly puppy. What we'll need is a smart contract language that was designed to empower people to write safe code from the start + an FV system + a FV DSL that regular devs can use to leverage FV's power without having to become an expert in it. This is, unsurprisingly, exactly the feature set we have built for Pact. If you think I missed/should add a feature for empowering safe contracts I'm all ears (seriously, criticism/ideas are always welcome). Wait a couple weeks and we'll have the public chain whitepaper(s) out (we're still refining the wording). [1]: https://youtu.be/Nw1glriQYP8?t=1072 https://youtu.be/Nw1glriQYP8?t=1072 -- my co-founder is presenting it [2]: http://kadena.io http://kadena.io [3]: "immutable code" gets you laughed out of the room in industry Edit: this came out when I was writing the response... are you planning to sell tokens in the system? If so, again, be careful. "SEC Issues Investigative Report Concluding DAO Tokens, a Digital Asset, Were Securities" https://www.sec.gov/news/press-release/2017-131 https://www.sec.gov/news/press-release/2017-131

nahollander 9y ago
Re: FV -- I admittedly have a surface level understanding of the entire subject matter. If you have any good primers and / or resources, I'd love to hear them. re: Pact -- sounds super cool. I look forward to reading the white paper. Would be happy to scan the drafts if you'd be interested in sharing too re: SEC -- just saw that too. I wouldn't say I totally disagree with the decision -- by Howie test standards, a governance token like DAO is functionally a security. Whether that jurisprudence will extend to grayer-area app coins and such is the real question. At the moment, not planning on a token sale. Largely because of the concerns you've alluded to.
- buckie 9y ago
  ### FV Resources These are few and far between. My paper on it is soup to nuts for how we do it in Pact which, while technical, should be somewhat approachable for most devs to grasp (I tried at least -- representing a program as equations is just an abstract concept). Until it comes out, the best one I've found as an entry point was the approach they use in Cryptol: https://youtu.be/ruNFcH-KibY?t=897 https://youtu.be/ruNFcH-KibY?t=897 . Cryptol, generally is a great project to look to for guidance. We're not going with the interactive approach. An EDSL in the docstrings is our approach so that you can pull a contract from the chain (pact is interpreted so the code on chain is the code that executes... well after it gets inlined and validated) and do the verification for yourself. Pact inlines at module creation/update time as a safety feature -- this way if a dep upgrades the code your contract runs doesn't change though the dep can revoke your code's right to access its tables/data until you update your contract. The "no leftpad" approach to deps. All the imported code that's pure, however, still works. This way, when you are building a module, you know that the code you formally verified/tested against is the only code that will ever run (until you update it). ### Whitepapers Thanks for the offer but I've already got enough people looking at them currently and we're keeping them confidential for now... a glaring stupid mistake would be embarrassing. Subscribe to the mailing list on kadena.io and you'll get updated with them the second they get released publically. ### SEC FYI I used to work at the SEC and I was their tech lead when they formed the Cryptocurrency Steering Committee, which has been renamed to the Distributed Ledger Technology Working Group (DLTWG). I worked with Valarie (then the head of it, still is probably) on a few actions. This is the group did the investigation and put out the release. Yep, no one is surprised by the take on the DAO and you're 100% right about the grayer-area of app coins. The key distinguisher will be, IMO, if the app-coin has real world use when it's sold + isn't supposed to return a profit as part of the app itself. IMO, expecting to resell the app-coins for a profit will be fine in the same way that art can be bought/sold for a profit, and a profit can be expected when one purchases it, but also art can be hung (or rented out and shown for a profit). Everything else is strictly a security.

by buckie 9y ago

nahollander 9y ago

Re: FV -- I admittedly have a surface level understanding of the entire subject matter. If you have any good primers and / or resources, I'd love to hear them. re: Pact -- sounds super cool. I look forward to reading the white paper. Would be happy to scan the drafts if you'd be interested in sharing too re: SEC -- just saw that too. I wouldn't say I totally disagree with the decision -- by Howie test standards, a governance token like DAO is functionally a security. Whether that jurisprudence will extend to grayer-area app coins and such is the real question. At the moment, not planning on a token sale. Largely because of the concerns you've alluded to.

buckie 9y ago
### FV Resources These are few and far between. My paper on it is soup to nuts for how we do it in Pact which, while technical, should be somewhat approachable for most devs to grasp (I tried at least -- representing a program as equations is just an abstract concept). Until it comes out, the best one I've found as an entry point was the approach they use in Cryptol: https://youtu.be/ruNFcH-KibY?t=897 https://youtu.be/ruNFcH-KibY?t=897 . Cryptol, generally is a great project to look to for guidance. We're not going with the interactive approach. An EDSL in the docstrings is our approach so that you can pull a contract from the chain (pact is interpreted so the code on chain is the code that executes... well after it gets inlined and validated) and do the verification for yourself. Pact inlines at module creation/update time as a safety feature -- this way if a dep upgrades the code your contract runs doesn't change though the dep can revoke your code's right to access its tables/data until you update your contract. The "no leftpad" approach to deps. All the imported code that's pure, however, still works. This way, when you are building a module, you know that the code you formally verified/tested against is the only code that will ever run (until you update it). ### Whitepapers Thanks for the offer but I've already got enough people looking at them currently and we're keeping them confidential for now... a glaring stupid mistake would be embarrassing. Subscribe to the mailing list on kadena.io and you'll get updated with them the second they get released publically. ### SEC FYI I used to work at the SEC and I was their tech lead when they formed the Cryptocurrency Steering Committee, which has been renamed to the Distributed Ledger Technology Working Group (DLTWG). I worked with Valarie (then the head of it, still is probably) on a few actions. This is the group did the investigation and put out the release. Yep, no one is surprised by the take on the DAO and you're 100% right about the grayer-area of app coins. The key distinguisher will be, IMO, if the app-coin has real world use when it's sold + isn't supposed to return a profit as part of the app itself. IMO, expecting to resell the app-coins for a profit will be fine in the same way that art can be bought/sold for a profit, and a profit can be expected when one purchases it, but also art can be hung (or rented out and shown for a profit). Everything else is strictly a security.