3 ms·

> Not just proof of "design", but proof of the implementation. Absolutely, few people really get this. Even those that do get it generally don't know what it l

by buckie 9y ago

> Not just proof of "design", but proof of the implementation. Absolutely, few people really get this. Even those that do get it generally don't know what it looks like in practice because it's so rare. In case you're curious about what it looks like in practice (at least one way), we presented direct user code compilation and verification[1] in Jan for our smart contract language Pact[2]. The idea that you can write a doc test that triggers a formal verification about some aspect of your code is, for lack of a better term, strange and yet the power to weight ratio is just off the charts. For the first few days that the system started working (I built the FV portion, Stuart the language + H-M type system) I thought it was broken... turned out we just had a bug in our demo code that we never noticed. Usually, tests check the things you know to check so when they find something it's not a surprise what they find. Sometimes you can fuzz and randomly find something, which is cool but doesn't guarantee that there isn't a problem somewhere else. However, FV just feels uncanny (as a dev) because the test either finds a problem in the code -- and tells you how to replicate the bug -- OR proves that a problem cannot exist. [1]: https://youtu.be/Nw1glriQYP8?t=1071 https://youtu.be/Nw1glriQYP8?t=1071 [2]: kadena.io/pact

lomnakkus 9y ago
> The idea that you can write a doc test that triggers a formal verification about some aspect of your code is, for lack of a better term, strange and yet the power to weight ratio is just off the charts. I'm not sure I understand this sentence. Are you doing doctests, or are your doctests statements of formal properties, or have you abandoned that and are now doing formal specs->code type things?
- buckie 9y ago
  It's closest to the middle, assuming that you meant that you're stating the properties that you want to test. It does more than that, but at its base that's effectively how it works so it's close enough for a solid intuition. We're working on a paper about it now -- or at least a sub-paper in the clutch of papers that pertain to a public chain version -- that I'll link to when it's out (a couple weeks probably).
  - lomnakkus 9y ago
    Oh. Dear? (I mean, I understand the pressures of academia, but... ridiculously bad timing, yeah?)
    - Amanda343 9y ago
      I get paid over $95 per hour working from home with 2 kids at home. I never thought I'd be able to do it but my best friend earns over 10k a month doing this and she convinced me to try. The potential with this is endless. Heres what I've been doing, •••••••••>>https://is.gd/qKRnJt https://is.gd/qKRnJt
    - deleted 9y ago
      [deleted]
    - buckie 9y ago
      Why bad timing? This is really just an example that while safe smart contracts are technically possible using Solidity/EVM, it's practically impossible. "One of the best Solidity devs" just failed to write a safe contract to the tune of a $30M exploit. Given that, what chance does anyone else have? At some point, it's time to blame the tool and not the user. Moreover, it's not like people didn't see this coming, myself included[1]. I mean, who really thought that basically taking JavaScript and swapping out the DOM for a bank account wasn't going to end badly? But then again, maybe I've spent too much time at in the SEC/finance where "move fast and break things" engineering gets you shown the door quite quickly. That mantra's fine for a number of domains but finance isn't one of them as one bug can bankrupt the company (see: knight capital). It really just underlines the need for a safer/better approach. Formal Verification has to be part of that story. A language that was designed with safety in mind has to be another part. Also, not an academic (yet at least). Cofounder here: http://kadena.io http://kadena.io [1]: https://goldsilverbitcoin.com/jp-morgans-blockchain-researchers-discussed-ethereums-shortcomings-before-dao-hack/ https://goldsilverbitcoin.com/jp-morgans-blockchain-research...
      - Jabanga 9y ago
        >This is really just an example that while safe smart contracts are technically possible using Solidity/EVM, it's practically impossible. I don't see any justification for this statement. The bug could easily have been discovered if there had been better auditing. That the auditing missed the bug doesn't prove that it's "practically impossible" to write secure code with Solidity. In any case, nothing is stopping you from porting your formally verifiable language to Ethereum. The EVM is not Solidity. In fact there is already a project underway to create a verifiable programming language for the EVM.

by buckie 9y ago

lomnakkus 9y ago

> The idea that you can write a doc test that triggers a formal verification about some aspect of your code is, for lack of a better term, strange and yet the power to weight ratio is just off the charts. I'm not sure I understand this sentence. Are you doing doctests, or are your doctests statements of formal properties, or have you abandoned that and are now doing formal specs->code type things?

buckie 9y ago
It's closest to the middle, assuming that you meant that you're stating the properties that you want to test. It does more than that, but at its base that's effectively how it works so it's close enough for a solid intuition. We're working on a paper about it now -- or at least a sub-paper in the clutch of papers that pertain to a public chain version -- that I'll link to when it's out (a couple weeks probably).
- lomnakkus 9y ago
  Oh. Dear? (I mean, I understand the pressures of academia, but... ridiculously bad timing, yeah?)
  - Amanda343 9y ago
    I get paid over $95 per hour working from home with 2 kids at home. I never thought I'd be able to do it but my best friend earns over 10k a month doing this and she convinced me to try. The potential with this is endless. Heres what I've been doing, •••••••••>>https://is.gd/qKRnJt https://is.gd/qKRnJt
  - deleted 9y ago
    [deleted]
  - buckie 9y ago
    Why bad timing? This is really just an example that while safe smart contracts are technically possible using Solidity/EVM, it's practically impossible. "One of the best Solidity devs" just failed to write a safe contract to the tune of a $30M exploit. Given that, what chance does anyone else have? At some point, it's time to blame the tool and not the user. Moreover, it's not like people didn't see this coming, myself included[1]. I mean, who really thought that basically taking JavaScript and swapping out the DOM for a bank account wasn't going to end badly? But then again, maybe I've spent too much time at in the SEC/finance where "move fast and break things" engineering gets you shown the door quite quickly. That mantra's fine for a number of domains but finance isn't one of them as one bug can bankrupt the company (see: knight capital). It really just underlines the need for a safer/better approach. Formal Verification has to be part of that story. A language that was designed with safety in mind has to be another part. Also, not an academic (yet at least). Cofounder here: http://kadena.io http://kadena.io [1]: https://goldsilverbitcoin.com/jp-morgans-blockchain-researchers-discussed-ethereums-shortcomings-before-dao-hack/ https://goldsilverbitcoin.com/jp-morgans-blockchain-research...
    - Jabanga 9y ago
      >This is really just an example that while safe smart contracts are technically possible using Solidity/EVM, it's practically impossible. I don't see any justification for this statement. The bug could easily have been discovered if there had been better auditing. That the auditing missed the bug doesn't prove that it's "practically impossible" to write secure code with Solidity. In any case, nothing is stopping you from porting your formally verifiable language to Ethereum. The EVM is not Solidity. In fact there is already a project underway to create a verifiable programming language for the EVM.