5 ms·

I'm curious: could any of the recently known smart contract bugs have been prevented through the use of a stricter type system? I tend to think of type systems

I'm curious: could any of the recently known smart contract bugs have been prevented through the use of a stricter type system? I tend to think of type systems more as a hindrance myself. I mean, they can certainly help you catch bugs before the code even runs - but which of those bugs would you not catch during the testing phase anyway? I'm genuinely curious: what types of bugs does a stricter type system catch that a reasonable test suite probably would not? Note I'm not saying that tests guarantee bug-free code, or that you can't do both. I'm just wondering about which different kinds of bugs you might catch.

relyio 9y ago
>I'm curious: could any of the recently known smart contract bugs have been prevented through the use of a stricter type system? Short-answer is yes, and there's been lots of work done to go even further than having static typing and have formal verification for smart-contracts. >I'm genuinely curious: what types of bugs does a stricter type system catch that a reasonable test suite probably would not? Not sure what you mean by "reasonable" (is it extensive? testing pathological cases? where do you draw the line?). But type checking at compile time makes your code less inclined to showcase a certain class of bugs that are the byproduct of ambiguity in the language semantics and logical mistake in the programmer writing the code. And with formal verification you can actually make sure that your logic meets the specs. You can hardly extract stronger correctness guarantees than that! If that interests you, check out Tezos (https://tezos.com/ https://tezos.com/) and github.com/tezos/tezos. The entire codebase is in OCaml. It was on the frontpage a while back: https://news.ycombinator.com/item?id=15061029 https://news.ycombinator.com/item?id=15061029
- jsnathan 9y ago
  > Short-answer is yes, and there's been lots of work done to go even further than having static typing and have formal verification for smart-contracts. Yes, I've looked at some of these projects before. And I certainly think it's a good idea to use automated tools to try to prove properties about programs. But I'm more excited about things like property testing than I am about things like strong type systems. And I'm wondering specifically what is the value they bring. No offense, but all of the answers I've gotten so far are very vague, and don't really address my question. I don't doubt that strong type systems can catch bugs, I am wondering how their capabilities in catching bugs differ from test suites. Let me give you an example, say we have a hypothetical language with a strict type system, and we declare a variable to be of type List[Foo]. Then later we use that variable as if it was really of type Foo. That's not gonna work, and a type-checker would catch that at compile-time. But a test suite (that covers the variable access) is going to catch that as well, because the code won't behave as it should. At which point is a strong type system going to surface a bug that a good test suite would not have? Like, can you give an example? > Not sure what you mean by "reasonable" (is it extensive? testing pathological cases? where do you draw the line?). The line is as variable as the strictness of the type system we would compare it to. I guess one could argue that a type system will force the programmer to satisfy it, while a test suite can be written very sloppily. So maybe there is some kind of signalling value in using these types of languages.
  - lomnakkus 9y ago
    > I am wondering how their capabilities in catching bugs differ from test suites. Well, for one they can prove the absence of certain classes of bugs. Buffer overflows, for example. No amount of testing can do that. Obviously most languages have "escape hatches" to do inherently 'unsafe' things like calling into C, but then at least you know exactly which bits to audit especially rigorously. > But a test suite (that covers the variable access) is going to catch that as well, because the code won't behave as it should. How many different List[X], where X != Foo do you need to test with to have the assurance you need? Are those tests that will actually get written? (IME it's pretty rare to see such "negative" tests, but then I mostly work in typed languages where such tests are usually unnecessary...) There's also the really huge advantage to types that they actually document a machine-checked contract in a way that integrates seamlessly with the language. There's no such consistency in e.g. JS-land. Now, those contracts may be pretty vague (in e.g. Java or C#), but in Haskell for example they include such things as "does this function have any side effects?". That's extremely powerful, but it's hard to appreciate just how powerful until you have experience in those type systems. EDIT: Also, don't forget that tests also have costs -- they have to be maintained just like the rest of the program, and static types can drastically cut down on the amount of tests you need to write+maintain.
  - yorwba 9y ago
    > I don't doubt that strong type systems can catch bugs, I am wondering how their capabilities in catching bugs differ from test suites. Type systems and test suites are complementary. When a test suite finds a bug, that proves that the program is incorrect for some inputs. When a type system doesn't reject a program, that proves that the program is correct for all inputs. Which one to use depends on the impact of an error. In the case of a system that controls lots of money, you'll want a guarantee that all inputs lead to a correct balance. That suggests to use a type system. On the other hand, if you're just writing an app to get data from a website and display it, you can probably afford it if the program doesn't work in some cases. If you can write a generator for realistic input, and check the output, that will give you a probabilistic estimate of correctness. The main advantage that test suites have over type systems is the kind of properties they can easily check. If you have a test suite that only checks that the output values have the right structure (EDIT: https://news.ycombinator.com/item?id=15137691 https://news.ycombinator.com/item?id=15137691 points out that part of the Lisk test suite does exactly that), you'd probably benefit even from the C type system. But to formalize the correctness of values, for many programs you'd need a much more powerful type system e.g. using dependent types, that isn't quite so simple to use as writing the equivalent test. I think a good compromise would be a language that allows you to annotate your types with arbitrary properties, but doesn't complain if it can't type-check them, so long as you write a test. (But it should complain when it can prove that the properties never hold, e.g. using success types, so that you don't waste time writing a test for that.)
protomikron 9y ago
> I'm genuinely curious: what types of bugs does a stricter type system catch that a reasonable test suite probably would not? Edge cases that you do not hit in your test cases. One could also argue that a distributed computing platform coupled to a money system may not need to be Turing complete. State-of-the art type systems are capable of proving non-trivial properties of code which could be handy in the crypto world.
syndev 9y ago
Sure, that could totally work. Part of the benefit a type system provides is that those checks are provided for you automatically, every time.
- jsnathan 9y ago
  Are we talking about automatic type inference then? Otherwise you'll still have to work out each type before it becomes "automatic". Which is not entirely dissimilar from working out a test suite.
kingmanaz 9y ago
Assuming stricter typing does prevent smart contract bugs, something like Ada or Spark would seem to be good fit for cryptocurrency development given their track record creating highly-reliable systems: https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language) That being said, I spent some time with Ada several years ago and did not enjoy the language; very verbose and anal. If the impression is widespread, such a language could end up hurting a blockchain project by drawing less contributors.
UncleMeat 9y ago
Yes. Here is one paper of interest https://www.comp.nus.edu.sg/~loiluu/papers/oyente.pdf https://www.comp.nus.edu.sg/~loiluu/papers/oyente.pdf.
- jsnathan 9y ago
  Hi, thanks for the link. I've seen this paper, but it has nothing to do with strongly typed languages, as far as I can tell. In fact, there is no mention of types in the paper at all, it's strictly automated analysis.

relyio 9y ago

>I'm curious: could any of the recently known smart contract bugs have been prevented through the use of a stricter type system? Short-answer is yes, and there's been lots of work done to go even further than having static typing and have formal verification for smart-contracts. >I'm genuinely curious: what types of bugs does a stricter type system catch that a reasonable test suite probably would not? Not sure what you mean by "reasonable" (is it extensive? testing pathological cases? where do you draw the line?). But type checking at compile time makes your code less inclined to showcase a certain class of bugs that are the byproduct of ambiguity in the language semantics and logical mistake in the programmer writing the code. And with formal verification you can actually make sure that your logic meets the specs. You can hardly extract stronger correctness guarantees than that! If that interests you, check out Tezos (https://tezos.com/ https://tezos.com/) and github.com/tezos/tezos. The entire codebase is in OCaml. It was on the frontpage a while back: https://news.ycombinator.com/item?id=15061029 https://news.ycombinator.com/item?id=15061029

jsnathan 9y ago
> Short-answer is yes, and there's been lots of work done to go even further than having static typing and have formal verification for smart-contracts. Yes, I've looked at some of these projects before. And I certainly think it's a good idea to use automated tools to try to prove properties about programs. But I'm more excited about things like property testing than I am about things like strong type systems. And I'm wondering specifically what is the value they bring. No offense, but all of the answers I've gotten so far are very vague, and don't really address my question. I don't doubt that strong type systems can catch bugs, I am wondering how their capabilities in catching bugs differ from test suites. Let me give you an example, say we have a hypothetical language with a strict type system, and we declare a variable to be of type List[Foo]. Then later we use that variable as if it was really of type Foo. That's not gonna work, and a type-checker would catch that at compile-time. But a test suite (that covers the variable access) is going to catch that as well, because the code won't behave as it should. At which point is a strong type system going to surface a bug that a good test suite would not have? Like, can you give an example? > Not sure what you mean by "reasonable" (is it extensive? testing pathological cases? where do you draw the line?). The line is as variable as the strictness of the type system we would compare it to. I guess one could argue that a type system will force the programmer to satisfy it, while a test suite can be written very sloppily. So maybe there is some kind of signalling value in using these types of languages.
- lomnakkus 9y ago
  > I am wondering how their capabilities in catching bugs differ from test suites. Well, for one they can prove the absence of certain classes of bugs. Buffer overflows, for example. No amount of testing can do that. Obviously most languages have "escape hatches" to do inherently 'unsafe' things like calling into C, but then at least you know exactly which bits to audit especially rigorously. > But a test suite (that covers the variable access) is going to catch that as well, because the code won't behave as it should. How many different List[X], where X != Foo do you need to test with to have the assurance you need? Are those tests that will actually get written? (IME it's pretty rare to see such "negative" tests, but then I mostly work in typed languages where such tests are usually unnecessary...) There's also the really huge advantage to types that they actually document a machine-checked contract in a way that integrates seamlessly with the language. There's no such consistency in e.g. JS-land. Now, those contracts may be pretty vague (in e.g. Java or C#), but in Haskell for example they include such things as "does this function have any side effects?". That's extremely powerful, but it's hard to appreciate just how powerful until you have experience in those type systems. EDIT: Also, don't forget that tests also have costs -- they have to be maintained just like the rest of the program, and static types can drastically cut down on the amount of tests you need to write+maintain.
- yorwba 9y ago
  > I don't doubt that strong type systems can catch bugs, I am wondering how their capabilities in catching bugs differ from test suites. Type systems and test suites are complementary. When a test suite finds a bug, that proves that the program is incorrect for some inputs. When a type system doesn't reject a program, that proves that the program is correct for all inputs. Which one to use depends on the impact of an error. In the case of a system that controls lots of money, you'll want a guarantee that all inputs lead to a correct balance. That suggests to use a type system. On the other hand, if you're just writing an app to get data from a website and display it, you can probably afford it if the program doesn't work in some cases. If you can write a generator for realistic input, and check the output, that will give you a probabilistic estimate of correctness. The main advantage that test suites have over type systems is the kind of properties they can easily check. If you have a test suite that only checks that the output values have the right structure (EDIT: https://news.ycombinator.com/item?id=15137691 https://news.ycombinator.com/item?id=15137691 points out that part of the Lisk test suite does exactly that), you'd probably benefit even from the C type system. But to formalize the correctness of values, for many programs you'd need a much more powerful type system e.g. using dependent types, that isn't quite so simple to use as writing the equivalent test. I think a good compromise would be a language that allows you to annotate your types with arbitrary properties, but doesn't complain if it can't type-check them, so long as you write a test. (But it should complain when it can prove that the properties never hold, e.g. using success types, so that you don't waste time writing a test for that.)

protomikron 9y ago

> I'm genuinely curious: what types of bugs does a stricter type system catch that a reasonable test suite probably would not? Edge cases that you do not hit in your test cases. One could also argue that a distributed computing platform coupled to a money system may not need to be Turing complete. State-of-the art type systems are capable of proving non-trivial properties of code which could be handy in the crypto world.

syndev 9y ago

Sure, that could totally work. Part of the benefit a type system provides is that those checks are provided for you automatically, every time.

jsnathan 9y ago
Are we talking about automatic type inference then? Otherwise you'll still have to work out each type before it becomes "automatic". Which is not entirely dissimilar from working out a test suite.

kingmanaz 9y ago

Assuming stricter typing does prevent smart contract bugs, something like Ada or Spark would seem to be good fit for cryptocurrency development given their track record creating highly-reliable systems: https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language) That being said, I spent some time with Ada several years ago and did not enjoy the language; very verbose and anal. If the impression is widespread, such a language could end up hurting a blockchain project by drawing less contributors.

UncleMeat 9y ago

Yes. Here is one paper of interest https://www.comp.nus.edu.sg/~loiluu/papers/oyente.pdf https://www.comp.nus.edu.sg/~loiluu/papers/oyente.pdf.

jsnathan 9y ago
Hi, thanks for the link. I've seen this paper, but it has nothing to do with strongly typed languages, as far as I can tell. In fact, there is no mention of types in the paper at all, it's strictly automated analysis.