7 ms·

Modelling financial contracts in an imperative event-driven paradigm just seems like an accident waiting to happen. EDIT: To the downvoters, if you disagree, I

by willtim 10y ago

Modelling financial contracts in an imperative event-driven paradigm just seems like an accident waiting to happen. EDIT: To the downvoters, if you disagree, I would very much like to understand why, please reply with a comment. EDIT2: My position is that it is very difficult to reason about correctness and maintain invariants in a highly imperative setting. IMHO, it would be more desirable to use a declarative, or functional language. There are many successful commercial applications of functional programming to financial contracts, e.g. Lexifi, which is based on a subset of OCaml and various in-house solutions developed by banks. Using a functional programming language would also mean the code is far more amenable to formal methods and static verification. One new startup I was very impressed with, aestheticintegration.com, has had success rewriting financial algorithms in a functional programming language in order to prove and verify numerous correctness properties about them. It is a huge shame that folk do not reach straight for the functional programming toolbox when faced with these types of problems.

rahimnathwani 10y ago
I didn't downvote you, but your comment left me scratching my head. You made a statement without any explanation. Care to elaborate why imperative programming is so bad here? Real-world contracts also use imperative style.
- jacquesm 10y ago
  This code is very bad, without going into an exhaustive enumeration, case sensitive function names, variables with unclear scope all over the place and so on. That it's imperative code is something that I don't think is damning by itself but all the side-effects (including side effects based on a single bit in the name of a function) really do warrant the 'accident waiting to happen'.
  - willtim 10y ago
    While personally I would prefer a functional approach, I take your point that a much more restrictive imperative setting would also be considerably better.
  - nawitus 10y ago
    > case sensitive function names Are you saying that function names should be case-insensitive?
    - jacquesm 10y ago
      No, I'm saying that if function names are case-sensitive that you're an idiot if you use that feature to distinguish between two functions otherwise named identically with different (important) side effects. The fact that the parameter set is different implies auto completion by an IDE was probably partially to blame here (if you did it by memory you'd have gotten a wrong parameter count warning). Some language features you best not exploit if you want to write reliable and bug-free (to whatever extent possible) code. This is not a typo so much as it is a very poor choice of naming convention.
    - kartickv 10y ago
      I'm not the OP, but I think they should be case-insensitive, if only to prevent errors like this. If you think otherwise, in what situation would it make sense to have two functions with names differing only in case? No upside, only a downside.
      - jacquesm 10y ago
        Case sensitive is fine if you throw an error when someone tries to define the same name with different case.
        kartickv 10y ago
        That gets us to 99% of what I had in mind, by preventing bugs like this one, but the remaining 1% is: why, then, generate an error when someone invokes a function while specifying a different case? If there's only one function, does the case matter?
- chii 10y ago
  real world contracts are interpreted by a court of law, which have leeways that aren't afforded by a machanical interpreter.
Waterluvian 10y ago
Same to you. Can you explain why you think so?
- willtim 10y ago
  I've tried to explain my position briefly above in an edit.
tmalsburg2 10y ago
This is the most insightful comment about this incident that I have seen so far. The problem is that the Etherum system uses an imparative language to describe smart contracts. This opens the door very wide for the kind of bugs that led to the theft of $200M from The DAO. The correct solution would probably have been to design a domain-specific declarative language that provides abstract building blocks for smart contracts. This would have allowed to hide the procedural complexity in the interpreter and contract bugs like the present one would not have been possible. Even if there was a problem, it could likely be fixed in the interpreter leaving the contracts and the blockchain untouched! This means that a lot of unanticipated problems would not have been fatal for the contracts. The problem of the current approach is that it conflates the business logic and it's implementation thus increasing the burden for contract authors and increasing the attack surface. In many other domains, a suboptimal choice of language paradigm would just add some extra friction but in the domain of smart contracts it can lead to catastrophic failures. Many people claim that the cause of the present disaster is just a faulty contract and that the Etherum system is working correctly. Some even say that the present case shows how well the technology is working. But willtim's comment makes it clear that there may be a fundamental problem with Ethereum. I wonder whether the imparative paradigm was a conscious design choice or something that just happened because the developers didn't even realize that it was a design choice. Edit: I wrote this before willtim's added his edit 2.
pron 10y ago
I think you are placing far too much emphasis on language, especially as so far there's little evidence that some programming approaches yield less logical errors than others. I often see a similar sentiment expressed by people who are familiar with functional programming but unfamiliar with software verification, and may be unaware that nearly all verified software in the industry is written in imperative languages. I know many FP people like to believe that the local guarantees made by their chosen languages end up making their programs more globally correct; it may well be true that some languages make some errors easier to spot for humans (although we have little evidence to suggest that this is indeed the case of FP). However, as far as formal verification is concerned, there is very little overlap between verified software and FP. Ensuring correctness -- i.e. conformance to a specification -- is, in general, a task that requires effort -- by man and/or machine -- proportional only to the complexity of the algorithm verified (i.e., the number of states reachable by a TM implementing it) and almost not at all to some linguistic properties. That is not to say that languages cannot prevent local errors that may be catastrophic, but the difference between the best of languages and the worst of languages when it comes to verifying spec-compliance is not that big. > Using a functional programming language would also mean the code is far more amenable to formal methods and static verification That is not true. If anything, imperative languages have better formal verification tools than functional ones. And besides, for global program "correctness" properties, the choice of a language more or less amenable to formal reasoning may make a difference that is surprisingly small.
- mbrock 10y ago
  I agree that functional vs imperative is a red herring in this case. The Ethereum model is "imperative" anyway, so a functional DSL would probably end up looking like some kind of monad. That said, it seems interesting to use a language like Agda for writing a DSL to EVM compiler, regardless of the exact nature of that DSL. Then you can have machine checked compiler correction proofs and also prove theorems about DSL programs.
  - pron 10y ago
    That would be interesting and even necessary. But why not use something much easier than Agda, though not less powerful for this use case -- like TLA+ -- something that even "ordinary" engineers could use to verify their contracts (not to mention that it supports model-checking in addition to deductive proofs, which reduces the verification effort considerably)?
johnbender 10y ago
I would go further. Given the sums of money involved I think it might also be worthwhile to have a formal semantics and a logic for proving safety properties of these blockchain programs (beyond type safety). Not every application would require that kind of rigour but if the participation and value of a given currency/contract/program is determined largely by trust then it seems natural to want more serious guarantees.
- willtim 10y ago
  I agree. I covered this only briefly under 'formal methods'. My point was that such formal semantics and proofs are far more easily obtained starting from a functional language.
- mietek 10y ago
  Note that a type system, if done properly, is simply another name for a logic for proving properties of programs. Examples: * Agda (http://wiki.portal.chalmers.se/agda/pmwiki.php http://wiki.portal.chalmers.se/agda/pmwiki.php) * Coq (https://coq.inria.fr https://coq.inria.fr) * Idris (http://www.idris-lang.org http://www.idris-lang.org)
jwr 10y ago
I partially agree — e.g. yes, declarative specifications would have been better. But having looked at some of the code, it's just poor quality. Bad code, plain and simple. If you write bad code, you will eventually get bitten. If you use bad code to build a financial institution with great claims, it will also cost you money and reputation. Bad engineering has consequences.
devit 10y ago
The actual issue is the fact that sending money to someone can result in untrusted code running in the middle of your code execution and even reentering it seems absurd. Sending should always succeed immediately and if anything needs to be automatically triggered in response, the trigger should be executed asynchronously. A great way to immediately see the problem is, for anyone with Rust experience, to think of this as a function taking an &mut self being somehow reentered without that &mut self being passed out by the function itself.
vessenes 10y ago
I completely agree. There seems to be less appetite for this than I would have imagined. A rich type system is absolutely going to be a huge help for smart contract authoring.

by willtim 10y ago

rahimnathwani 10y ago

I didn't downvote you, but your comment left me scratching my head. You made a statement without any explanation. Care to elaborate why imperative programming is so bad here? Real-world contracts also use imperative style.

jacquesm 10y ago
This code is very bad, without going into an exhaustive enumeration, case sensitive function names, variables with unclear scope all over the place and so on. That it's imperative code is something that I don't think is damning by itself but all the side-effects (including side effects based on a single bit in the name of a function) really do warrant the 'accident waiting to happen'.
- willtim 10y ago
  While personally I would prefer a functional approach, I take your point that a much more restrictive imperative setting would also be considerably better.
- nawitus 10y ago
  > case sensitive function names Are you saying that function names should be case-insensitive?
  - jacquesm 10y ago
    No, I'm saying that if function names are case-sensitive that you're an idiot if you use that feature to distinguish between two functions otherwise named identically with different (important) side effects. The fact that the parameter set is different implies auto completion by an IDE was probably partially to blame here (if you did it by memory you'd have gotten a wrong parameter count warning). Some language features you best not exploit if you want to write reliable and bug-free (to whatever extent possible) code. This is not a typo so much as it is a very poor choice of naming convention.
  - kartickv 10y ago
    I'm not the OP, but I think they should be case-insensitive, if only to prevent errors like this. If you think otherwise, in what situation would it make sense to have two functions with names differing only in case? No upside, only a downside.
    - jacquesm 10y ago
      Case sensitive is fine if you throw an error when someone tries to define the same name with different case.
      - kartickv 10y ago
        That gets us to 99% of what I had in mind, by preventing bugs like this one, but the remaining 1% is: why, then, generate an error when someone invokes a function while specifying a different case? If there's only one function, does the case matter?
chii 10y ago
real world contracts are interpreted by a court of law, which have leeways that aren't afforded by a machanical interpreter.

Waterluvian 10y ago

Same to you. Can you explain why you think so?

willtim 10y ago
I've tried to explain my position briefly above in an edit.

tmalsburg2 10y ago

This is the most insightful comment about this incident that I have seen so far. The problem is that the Etherum system uses an imparative language to describe smart contracts. This opens the door very wide for the kind of bugs that led to the theft of $200M from The DAO. The correct solution would probably have been to design a domain-specific declarative language that provides abstract building blocks for smart contracts. This would have allowed to hide the procedural complexity in the interpreter and contract bugs like the present one would not have been possible. Even if there was a problem, it could likely be fixed in the interpreter leaving the contracts and the blockchain untouched! This means that a lot of unanticipated problems would not have been fatal for the contracts. The problem of the current approach is that it conflates the business logic and it's implementation thus increasing the burden for contract authors and increasing the attack surface. In many other domains, a suboptimal choice of language paradigm would just add some extra friction but in the domain of smart contracts it can lead to catastrophic failures. Many people claim that the cause of the present disaster is just a faulty contract and that the Etherum system is working correctly. Some even say that the present case shows how well the technology is working. But willtim's comment makes it clear that there may be a fundamental problem with Ethereum. I wonder whether the imparative paradigm was a conscious design choice or something that just happened because the developers didn't even realize that it was a design choice. Edit: I wrote this before willtim's added his edit 2.

pron 10y ago

I think you are placing far too much emphasis on language, especially as so far there's little evidence that some programming approaches yield less logical errors than others. I often see a similar sentiment expressed by people who are familiar with functional programming but unfamiliar with software verification, and may be unaware that nearly all verified software in the industry is written in imperative languages. I know many FP people like to believe that the local guarantees made by their chosen languages end up making their programs more globally correct; it may well be true that some languages make some errors easier to spot for humans (although we have little evidence to suggest that this is indeed the case of FP). However, as far as formal verification is concerned, there is very little overlap between verified software and FP. Ensuring correctness -- i.e. conformance to a specification -- is, in general, a task that requires effort -- by man and/or machine -- proportional only to the complexity of the algorithm verified (i.e., the number of states reachable by a TM implementing it) and almost not at all to some linguistic properties. That is not to say that languages cannot prevent local errors that may be catastrophic, but the difference between the best of languages and the worst of languages when it comes to verifying spec-compliance is not that big. > Using a functional programming language would also mean the code is far more amenable to formal methods and static verification That is not true. If anything, imperative languages have better formal verification tools than functional ones. And besides, for global program "correctness" properties, the choice of a language more or less amenable to formal reasoning may make a difference that is surprisingly small.

mbrock 10y ago
I agree that functional vs imperative is a red herring in this case. The Ethereum model is "imperative" anyway, so a functional DSL would probably end up looking like some kind of monad. That said, it seems interesting to use a language like Agda for writing a DSL to EVM compiler, regardless of the exact nature of that DSL. Then you can have machine checked compiler correction proofs and also prove theorems about DSL programs.
- pron 10y ago
  That would be interesting and even necessary. But why not use something much easier than Agda, though not less powerful for this use case -- like TLA+ -- something that even "ordinary" engineers could use to verify their contracts (not to mention that it supports model-checking in addition to deductive proofs, which reduces the verification effort considerably)?

johnbender 10y ago

I would go further. Given the sums of money involved I think it might also be worthwhile to have a formal semantics and a logic for proving safety properties of these blockchain programs (beyond type safety). Not every application would require that kind of rigour but if the participation and value of a given currency/contract/program is determined largely by trust then it seems natural to want more serious guarantees.

willtim 10y ago
I agree. I covered this only briefly under 'formal methods'. My point was that such formal semantics and proofs are far more easily obtained starting from a functional language.
mietek 10y ago
Note that a type system, if done properly, is simply another name for a logic for proving properties of programs. Examples: * Agda (http://wiki.portal.chalmers.se/agda/pmwiki.php http://wiki.portal.chalmers.se/agda/pmwiki.php) * Coq (https://coq.inria.fr https://coq.inria.fr) * Idris (http://www.idris-lang.org http://www.idris-lang.org)

jwr 10y ago

I partially agree — e.g. yes, declarative specifications would have been better. But having looked at some of the code, it's just poor quality. Bad code, plain and simple. If you write bad code, you will eventually get bitten. If you use bad code to build a financial institution with great claims, it will also cost you money and reputation. Bad engineering has consequences.

devit 10y ago

The actual issue is the fact that sending money to someone can result in untrusted code running in the middle of your code execution and even reentering it seems absurd. Sending should always succeed immediately and if anything needs to be automatically triggered in response, the trigger should be executed asynchronously. A great way to immediately see the problem is, for anyone with Rust experience, to think of this as a function taking an &mut self being somehow reentered without that &mut self being passed out by the function itself.

vessenes 10y ago

I completely agree. There seems to be less appetite for this than I would have imagined. A rich type system is absolutely going to be a huge help for smart contract authoring.