4 ms·

It's a good indicator that these people may be experts in one area, but not necessarily in others. Language design is actually notoriously difficult in general

It's a good indicator that these people may be experts in one area, but not necessarily in others. Language design is actually notoriously difficult in general[1], but if you're doing language design for a security-critical language[2]... well, that requires actual mechanized proof, IMO. Not just proof of "design", but proof of the implementation. Anything else is a huge gamble. (And I'm sure there are some 'investors'/gamblers who made off very well.) [1] Beyond surface-level, obviously. [2] We're talking about 0.0001% of the general population here.

Claire88 9y ago
my stepmother recently got a nice twelve month old Nissan Rogue SUV only from working part time off a macbook air. visit this page>>>>>>>>http://www.joinmate2.com http://www.joinmate2.com chek it site.
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...
goldfeld 9y ago
Experts in what area? Not in programming, to think exposing functionality by default is a good design concept.

Claire88 9y ago

my stepmother recently got a nice twelve month old Nissan Rogue SUV only from working part time off a macbook air. visit this page>>>>>>>>http://www.joinmate2.com http://www.joinmate2.com chek it site.

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...

goldfeld 9y ago

Experts in what area? Not in programming, to think exposing functionality by default is a good design concept.