Hacker News Reader

Comment by willtim | Hacker News Reader

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.

View on HN

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.

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.

Of course most of the money has been funding tools for imperative languages as that is the status quo. But this does not prove that there is little overlap with FP. Research FP languages like Coq have enabled INRIA to build a fully verified C compiler (Compcert), can your tools accomplish this? As far as Europe is concerned, FP does appear to be the future of formal verification.

> Research FP languages like Coq have enabled INRIA to build a fully verified C compiler (Compcert), can your tools accomplish this?

First of all, end-to-end verification is something very unique. CompCert is a great accomplishment, but it is only a medium-sized program, it required a world-expert to write, and even then it tool a lot of effort and still he skimped on the termination proofs.

Imperative tools, OTOH, are used every day by thousands of engineers to write verified software of various kinds (e.g., [1]). So the answer to your question is: except for end-to-end verification, which is extremely costly with any approach, they can do better. In fact, as promising as FP approaches may be, they are still very much in the lab with nearly negligible industry use (and in the one or two cases Coq has been used in the industry, it was always done jointly with academics).

Also, I'm a bit puzzled because you specifically mentioned OCaml, which is an imperative functional language.

In fact, while the difference between programming language in terms of general amenability to formal methods is not great, there are certainly large differences in amenability to model checking. This is why a language like SCADE (based on Esterel and the FRP-ish Lustre) is a fairly widely used tool in aviation software. If anything, a synchronous language like Esterel or the modern Céu[2] are a better choice if you want your verification to be as automatic as possible and run in a resource-constrained environment (that's killing two birds with one stone).

> As far as Europe is concerned, FP does appear to be the future of formal verification.

Even if you look at INRIA, the most European of institutions and the birthplace of Coq, you'll see that they dedicate significant verification research to other approaches[3]. At Max Planck, FP is a clear minority[4].

And if you look at the academic community at large without artificially restricting it to Europe (which certainly has a linguistic bias), you'll see that the verification community is certainly not betting on FP (although they are certainly exploring it). Don't get me wrong: FP and linguistic approaches is certainly one avenue among several showing promise in verification. But it is downright false to say that this approach is recognized as "the future of verification".

[1]: https://verificationinstitute.org/wp-content/uploads/sites/2...

[2]: http://www.ceu-lang.org/

[3]: http://www.inria.fr/en/teams/veridis

[4]: http://plv.mpi-sws.org/

I mentioned Lexifi, a contract language, which is based on OCaml and is not imperative. I restricted my argument to Europe as we appear to be less commercially influenced (e.g. MIT teach freshmen Python, Oxford teach Haskell). Predicting the future is always subjective. I offered only my opinion.

> I mentioned Lexifi, ... which is based on OCaml and is not imperative.

Oh, sorry.

> we appear to be less commercially influenced

I don't think this has anything to do with commercial influence -- just academic tradition and maybe even philosophical influences: I think you'll get different answers to the question, "does an algorithm or a computation exist outside its description in a language, and if so, in what way?" This may be tied to actual philosophies, Derrida in France vs. Kripke in the US[1] (to prove the connection, a "Kripke structure" is a very common mathematical structure denoting an "abstract" computation, which is used commonly in non-language-based verification). I've been told that the study of program semantics tries to reconcile the two.

As to Haskell vs. Python, first, MIT used to teach Scheme; they have explained their reasons for switching to Python. Second, this difference is more indicative of the competition between "theory A" and "theory B". Theory A studies algorithms and complexity (and Haskell is not the best first pedagogical choice for that), while theory B studies logic and semantics (and language). Theory B is relatively small, but it does have a stronger presence in Europe. Although, even within theory B there seem to be those who prefer linguistic approaches (semantics) and those who prefer conceptual approaches (Kripke structures, abstract machines).

[1]: Not that Britain is too fond of French philosophy, but the Brits had Robin Milner, who is as close to a CS deconstructionist as you could find.

It's worth pointing out that most of the formal methods you have linked to involve contracts or specifications as separate stratified layers written in various logics. No Turing Machines involved. This is essentially functional programming as far as I'm concerned. The advantage of the dependant-type approaches like Coq and Agda, is that the language of proof and implementation is now one of the same, but I was not necessarily advocating their use as you seem to have assumed. Even without dependent types, a total functional program can serve as both an executable specification and a logic with which one can derive proofs from (e.g. via an SMT solver). This is what I meant when I said functional programming is more amenable to formal methods. So any tool that uses dataflow analysis to convert imperative programs into functional ones, or requires me to write functional programs to describe what the imperative program should be doing, doesn't provide a counter argument in my mind. Finally, in my very first comment, I provided a link to a startup who are planning on using FP and SMT solvers for formal verification of blockchain contracts, so watch this space...

> No Turing Machines involved.

When are Turing machines ever involved? Verification tools often make use of abstract state machines as the subject of their study. I am not aware of a single one that deals with Turing machines (nor am I aware of a single TM programming language being used in the industry). TMs serve an important role in theoretical computer science, in automata theory and complexity theory, but not in verification or PL.

> This is essentially functional programming as far as I'm concerned.

It isn't. Logic was applied to programs long before FP was in vogue.

> The advantage of the dependant-type approaches like Coq and Agda, is that the language of proof and implementation is now one of the same,

Two things. First, you can implement a system in Isabelle, too. Second, that advantage -- if it is one -- is rather theoretical at this point. Dependently typed languages have never been used outside of the lab, and have never been used in a large project. The approach, BTW, has plenty of disadvantages. First, the languages are very hard to learn, and require some very exotic, obscure math; second, some very important properties like time and space complexity -- that are often just as essential as logical correctness for those application where correctness matters most -- are hard to express, and there's no consensus yet on how to best reason about them. In short, dependent type approaches may one day be useful, but in general, we're not sure exactly how to use them yet.

> a total functional program can serve as both an executable specification and a logic with which one can derive proofs from

That is absolutely true, but this has some very severe disadvantages as well.

> so watch this space...

I have no doubt. But you should be aware that FP approaches to verification are just some of the many avenues in verification research these days, and are not generally accepted to be the most promising ones. In addition, unlike other approaches, they have pretty much never been put to the test outside the lab. Finally, SMT solvers are successfully used to verify Java programs (with JML specifications), and in the research world, Microsoft's Dafny[1] -- an imperative, non-functional (I think) language -- is a very popular choice in verification challenges (alongside tools like KIV[2] and Why3[3]). They also, I think, serve as the core proof method of SPARK Ada, a heavy duty verifiable language, with a good track record over many years in the industry.

[1]: http://research.microsoft.com/en-us/projects/dafny/

[2]: http://www.isse.uni-augsburg.de/en/software/kiv/

[3]: http://why3.lri.fr/

> When are Turing machines ever involved?

Most software is written in imperative Turing equivalent languages, so Turing Machines are involved all the time. The fact that most verification software is not capable of dealing with them, demonstrates a language issue. Which is the point I have been trying to make.

> It isn't. Logic was applied to programs long before FP was in vogue.

I'm advocating modelling contracts with Logic, instead of Turing Machines as used by Ethereum. I didn't mean to create a tribal boundary by using the term FP.

> Most software is written in imperative Turing equivalent languages, so Turing Machines are involved all the time.

I don't understand what that means. Everything is "Turing equivalent" in some sense[0]. It's like saying that since every language can be compiled to C, then C is "involved all the time". That would even be more accurate, because our programs are most certainly not TM-equivalent. Proof: the asymptotic complexity of a real program and that of a Turing machine for most algorithms differs by a power of 2 or 3. Therefore, programs and TMs cannot possibly be equivalent. If you had said RAM machines at least you would have been somewhere in the ballpark, and RAM machines are not Turing machines (see https://en.wikipedia.org/wiki/Random-access_machine).

> The fact that most verification software is not capable of dealing with them, demonstrates a language issue.

But that is not a fact, because 99% of the thousands of very real, verified production systems being constantly worked on are written in imperative languages, and roughly 0-1% is written in functional languages. Quite the contrary, verification software handles imperative programs better than functional programs. You don't have to take my word for it. See what one Xavier Leroy (author of CompCert) says on the issue here[1] and here[2]. So far, verification in functional languages requires inordinate effort.

The question of how much verification is tied to language is very much an open question.

> I'm advocating modelling contracts with Logic, instead of Turing Machines as used by Ethereum.

I wonder what you'd say about temporal logic, which is not only the most popular logic in software verification but one that models state machines.

As to Turing machines, I don't think you understand what they are. A Turing machine is one particular automaton, a particular instance of an abstract state machine, and a universal computational model, which is usually applied directly only in computational complexity theory, where it serves as a common cost model. The lambda calculus is a rewriting system (typed versions of which can be tied to one particular kind of logical reasoning via the C-H correspondence), another universal model of computation, and -- guess what -- another instance of an (ND) abstract state machine!

In short there are many concepts here that you mix up. Turing machines, however, are one concept that is completely absent from both PLs and software verification (where it tends to turn up only in the marketing speech of some FP advocates). No one programs Turing machines. Program logics most certainly apply to imperative languages, and in fact, this is -- to date -- where they are most used, and quite successfully.

[0]: And if you're referring to total languages then you're confusing things further. Totality has little effect on verification; it is required in order to not introduce logical inconsistencies in typed lambda calculus, and is only relevant when dependently typed languages are used to prove general mathematical theorems -- not verify programs.

[1]: http://events.inf.ed.ac.uk/Milner2012/X_Leroy-html5-mp4.html

[2]: http://events.inf.ed.ac.uk/Milner2012/Monday_Panel-html5-mp4...

I can assure you I understand what a Turing machine is. I brought them up because the less powerful abstract machines you mentioned are not sufficient to (fully) express Ethereum or most other mainstream imperative languages. You seem to argue that imperative programming is just as mathematically rigorous as FP, because one can have abstract state machines in mind, yet strongly object when I compare Ethereum to a Turing Machine. You also appear to suggest that formal verification has no problem dealing with computations that require Turing equivalence (by dismissing my point as 'false') and then state that Turing Machines have no place in formal verification. If I sound mixed up it's because I'm trying to make sense of your position.

> Everything is "Turing equivalent"

This doesn't make any sense. As you say, there are less powerful automatons. A programming language does not need to support universal computation, for example Unix RegEx.

I cannot disagree that imperative programming is more popular, but again that is no proof that we are better of using them is we want to easily build correct software.

> because the less powerful abstract machines you mentioned are not sufficient to (fully) express Ethereum or most other mainstream imperative languages.

No, again -- you are confusing specific machines (like TMs) with abstract state machines. Abstract state machines are a super-set of Turing machines (some are equivalently powerful in terms of computability, albeit "faster" wrt time complexity -- e.g. lambda calculus or RAM machines; others are less powerful). But Ethereum is not a Turing machine, just like Haskell isn't. Turing machines are a very specific thing, like x86 assembly. Ethereum is not based on x86 assembly, just like it isn't based on Turing machines.

> but again that is no proof that we are better of using them is we want to easily build correct software.

I agree; I didn't say they're any better. But you claimed that FP is better, and there's certainly no evidence to support that. Some extremely powerful formal verification tools, however, currently have no good, production-quality applications for FP.

The confusion here is that you repeatedly seem to misunderstand my point, perhaps that is my fault as I do not have the time to write very carefully (e.g. I've used "Turing Machine" as a cheap shot at imperative programming). You even stated it yourself earlier "because our programs are most certainly not TM-equivalent". If you agree that most programs do not require Turing equivalence, then you must surely understand my main point, which is why provide powerful expressive languages that, for example, do allow Turing complete computations. Does a contract language, or even a systems language need to really support Turing completeness? You seem to argue that it doesn't matter. I think it does.

Oh, you are right that finite-state machines make automated verification easier (assuming that by Turing machine you meant Turing complete). However, some people are under the impression that other sub-Turing-complete languages (in particular, total functional programs) are easier to verify than programs in Turing-complete languages. This is false. The only class of languages that are practically "easy" to verify are finite state machines (well, if you call being PSPACE-complete easy; even that is exponential in the program's size!). This is easy to prove (in fact, it is a simple corrolary of the time hierarchy theorem and its proof). In particular, it is trivial to show that the problem of verifying a program in a total language is harder than any problem with a computable complexity bound, i.e. it's complexity is non-computable, i.e. it has "busy beaver" complexity[1]. I'm giving a talk on this precise subject next month at Curry On (http://curry-on.org/2016/sessions/why-writing-correct-softwa...)

[1]: The difference, therefore, between verification of Turing-complete programs and total programs is that the cost of verifying the former in the general case is infinite, while the cost of the other grows like some function that is larger than any function we can ever compute. From the perspective of computing power, both are equally beyond reach.

That looks like a great talk, I hope it will be recorded.

I've just now watched the talk [1], thank you for the link, but I feel his conclusion actually backs up my position: "Pure, strict functional programming is a very short path from a program to a correctness proof". Admittedly, the tooling in this area has yet to arrive. But for a bespoke contracts language, I wouldn't be put off by that.

Well, I'd be very surprised if Leroy had said anything else. FP is his field, after all. But this view is far from the consensus in the software verification community. Bear in mind, though, that both (somewhat intersecting) disciplines of PL (especially FP) and formal methods have a lot to answer for. Both have made a lot of grand promises over the past 30 years, and both have failed to deliver anything near what they'd promised.

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.

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)?

Maybe that would be better. I admit that I don't know the first thing about TLA+. Agda is what I learned about in school, and what my computer science friends are excited about, and I was already interested in using it to write verified compilers. Writing compilers with functional languages was also a part of my university education. But that's just my background.

I see parallels here with UI code that is very imperative in nature, but FRP and similar approaches are showing great promise in creating abstractions for reasoning.

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.

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.

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)

* Coq (https://coq.inria.fr)

* Idris (http://www.idris-lang.org)

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.

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.

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.

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

While personally I would prefer a functional approach, I take your point that a much more restrictive imperative setting would also be considerably better.

> case sensitive function names

Are you saying that function names should be case-insensitive?

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.

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.

Case sensitive is fine if you throw an error when someone tries to define the same name with different case.

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?

real world contracts are interpreted by a court of law, which have leeways that aren't afforded by a machanical interpreter.

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.

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

I've tried to explain my position briefly above in an edit.

Reply on news.ycombinator.com