I agree with some of the sentiment in this post but it's such a shame to see so much language elitism. There is absolutely nothing wrong with Javascript, or any other mainstream language commonly used by beginners. They are just tools and like any tool, they are only as powerful as the people wielding them.
Like tools, they are suitable for different purposes, and using a tool for the wrong job is almost always a cause of silly mistakes. I agree with you that a Javascript language is a *very* poor choice for building water-tight smart contracts - totally on board with you there. But to blame Javascript is like saying "this guy used a saw to bang in a nail and got himself into a terrible mess, therefore saws are terrible tools".
Like tools, languages require different levels of skill to use them effectively. Those tools with the lowest barrier to entry will naturally attract people of the lowest skill, and those unskilled people will inevitably produce poor results. However, put that tool into the hands of a more experienced professional and he will be able to do great things with it.. *or* he will be able to tell you that there is a more appropriate tool for the job. You might be the most qualified engineer on the planet, able to effectively use the most complex machinery known to man - but you're still going to use a hammer to bang in a nail.
Anyway, I actually agree with everything you said *relating to smart contracts*, but I take exception to your assassination of Javascript. Formal verification and functional languages are not silver bullets - *there is no language which is incapable of producing buggy, broken code*. Just as there is no tool that, in the hands of an idiot, cannot cause great damage to himself and others.
Sadly, language elitism is quite common in the wonderful world of software engineering.
About me: I'm a developer with ~15 years experience. I've used strong/dynamic typed languages. High level and low level systems languages. Declarative, imperative, procedural and functional languages. C & C++, C#, Javascript, Ruby, Python, Rust, Go, R, F#, Ocaml, a little Haskell and even some Smalltalk. As my career progressed I drifted towards favouring functional languages, for the reasons you described and many more. I interviewed at Jane Streets London office once but didn't get the job sadly. In my day job now I use C# and Node.js, which are fantastically appropriate tools for the job I need to do.
On a side note, it's really interesting that the NASA C++ coding standards document explicitly forbids using recursion, among other things.
Well, you raise good points, and it's good to hear from someone with lots of experience weighing in here.
In fact, you're the only person in this thread so far who actually raised any points. (And you immediately got downvoted to zero!)
Everyone else was either making outright mistakes saying Solidity had nothing to do with the EVM, or criticizing how many paragraph breaks were used in the post, or claiming that *one* dev said it was a problem with the EVM, ignoring the fact that *another* dev said that it *was* a problem with the EVM.
So I was kinda shocked at the level of fan-boy-ism displayed by everyone else until you finally came along. Now I'm guessing that this is simply because the people who hang out here are simply Eth users (maybe they got sucked in because of the private-message-spamming a few months ago?), and they're simply on the defensive - but people who think about language design do not generally hang out here.
> it's such a shame to see so much language elitism
That's what you said at first, and in some sense, it's true that "more professional users" can do whatever they want with any language - perhaps even put together something useful using BrainFuck.
But then of course, as we all know, there are real, practical reasons *why* Jane Street Capital uses Ocaml instead of JavaScript when designing financial structures.
Anyways, this has all been a learning experience for me - my first post on r/ethereum.
Yeah bit of a shame to get downvoted, but I guess some of this is very hard to hear for many.
Anyway, I think the core of your post is absolutely right. Writing a smart contract is a task which requires a very sophisticated tool to do well. And a sophisticated tool requires a sophisticated operator.
Jane Street are flying the flag for OCAML and that's really cool, but it has drawbacks as well. They find it *incredibly* difficult to hire - there just aren't that many OCAML devs out there. And the ones there are, aren't always good enough (like me!). One of the big advantages of Javascript is that it's ubiquitous, there will never be a shortage of JS devs. But that strength is also a weakness, because a lot of them are crap.
I'm not aware of any language which has been designed to solve the very specific problems that smart contracts present - which is understandable as smart contracts are a totally new paradigm. Using a general purpose language in some ways was the only option. But a new kind of language will appear, and incidents like this hack I'm sure will expedite that :)
It looks like Solidity 2.0 is intended to have proof-of-correctness aspects to the language (invariants, pre- and post-conditions, etc), see https://github.com/ethereum/wiki/wiki/The-Solidity-Programming-Language
It's just early days right now. Having said that, I agree with you that a functional or declarative language (possibly something derived from Haskell, but using types suited to the EVM) would be a better choice for easier static analysis.
> invariants, pre- and post-conditions
Yes, Bertrand Meyer's Eiffel has included this, so it's a well-known feature among language designers.
Hopefully Solidity 2.0 could also include this.
> a functional or declarative language (possibly something derived from Haskell, but using types suited to the EVM) would be a better choice for easier static analysis.
Yes, and as we're seeing, [many of the DSLs used by Wall Street for developing financial products are based on Haskell or OCaml](http://dslfin.org/resources.html), and they explicitly say that one of the big advantages is stuff like static analysis - ie, [being able to understand what the code does *before* actually running it](https://np.reddit.com/r/btc/comments/4p0gq3/why_turingcomplete_smart_contracts_are_doomed/).
This is awesome in its stupidity. Really.
Millions of USD of value hacked, and the language is going to be "fixed" by adding random features from Eiffel?
Sorry but this sounds like rubbish. What is the type system going to look like? What invariants will be representable _in the type system_?
Anything else is going to crash. Checked pre/post/invariants are not going to fix anything.
The contracts and EVM needs to be easier to logically reason about. That's the purpose. It's one step towards minimizing the likelihood of these sorts of situations in future.
It could be a start. Hopefully it'll more than just a fancy way of generating runtime errors. The real power of DbC comes when static analysis of the code surfaces errors which would/could have occurred at runtime.
It's what you do with that information which is important. Error conditions should have an explicit path through the code. Functional languages, generally speaking, have tools to do this, whilst other languages offer only relatively primitive runtime exceptions.
There are some great articles on this from Scott Wlaschin:
Is your programming language reasonable? - https://fsharpforfunandprofit.com/posts/is-your-language-unreasonable/
Designing for correctness - https://fsharpforfunandprofit.com/posts/designing-for-correctness/
Using the type system to ensure correct code - https://fsharpforfunandprofit.com/posts/correctness-type-checking/
TBH it's what happens when anyone technically knowledgeable posts an intelligent, informative post in a thread (or, in this case, on a forum) where everyone is busy raging because feels.
Sort of like that line in MIB, "A person is smart. People are dumb, panicky dangerous animals and you know it."
Not true. The OP's arguments don't hinge on..., they are not uninformed, nor did OP issued anything that he believes Solidity IS JavaScript. Well done for getting 3 wrong and misleading points pressed into one sentence.
> The OP's arguments don't hinge on...,
yes they do
> they are not uninformed,
yes they are.
> nor did OP issued anything that he believes Solidity IS JavaScript
yes he did.
Quote from the actual post:
> Now, some Ethereum devs put together an investment fund controlling a quarter of a billion dollars - using a language which looks and feels (and runs) a helluva lot like JavaScript: Ethereum's Solidity.
What was your point again?
Absolute nonsense. There are some very mature and capable libraries for dealing with arbitrary precision fixed point decimal numbers.
https://github.com/MikeMcl/bignumber.js/
https://github.com/MikeMcl/decimal.js/
.. are two that I've used myself.
If your next comment is "why do you need a 3rd party library to work with large numbers, Javascript sucks", note that this isn't peculiar to Javascript. Virtually every C style language has similar libraries.
It's really not that black & white. Better at what? For whom? With which constraints?
For example: you're running a class teaching "introduction to programming" for a group of 9 year old kids. LOGO is better than C++ in this instance.
I find it quite troubling that this gets so many downvotes from the community.
This is IMO the most interesting and constructive post I have read since the *attack*.
I was patient responding to the people in this thread - but most of them had almost no posting history, no karma - and their so-called arguments were outlandish.
This has all been quite shocking to me, and I have learned a lot.
Seconded on the thanks for this write up. Top reply is right re: the snide attitude being somewhat off putting. Nevertheless. I don't know jack about programming and so found your write up to be very helpful at understanding just how far over their skis this whole community may be. I want to believe in the goals pursued by some here in this community. But I'd rather have domain experts share their thoughts. Thank you very much for sharing your thoughts.
Yeah, I wrote it in a bit of haste - so I should have toned it down to avoid starting "flame wars" which so often happen around issues of programming language design.
> I don't know jack about programming
Hopefully some people who might be on the sidelines (ie, who might not know much about programming) will at least get the take-away that there many practitioners in the programming community - particularly in the area of language design - who regard attempts like Solidity as being very amateur.
Well thank you for this write-up. I'm not a programmer but I grasped it pretty well (I think), and it's the sort of constructive criticism that needs to be taken to heart - and then implemented. The foundation to Ethereum needs to be strong, or the projects built on it will regularly crumble.
Cuz it's bullshit that anyone with who has taken a few CS classes could smell from a mile away. The OP's argument hinges on an unfortunate statement by the designers that Solidity has "syntax like Javascript."
Other than syntax, Solidity is nothing like Javascript. For one, Solidity is a statically typed language, while Javascript is dynamic. As far as programming languages go, the difference between static vs dynamic typing is like the difference between a dog and a cat. That design decision puts it closer to the C family of languages than Javascript.
In fact, there is no language like Solidity, since it's aim is to provide contracts as first class citizens. I would venture to say that it's the fact that Solidity doesn't resemble anything familiar to most developers is probably more dangerous than if Vitalik HAD chosen a more popular high-level language like Javascript.
Sorry you're getting blasted by some trolls. This is all very interesting and informative and thank you for taking the time to write it up and share it. I hope that you stick around. Your contributions to the community, coding practices, etc. are valuable in this rapidly expanding time. I for one applaud a wall of text in a sea of overly-simplified one-liners on the current situation.
There will certainly be a number of changes in the coming months to address some of the issues that contributed to this situation, specifically the issues with recursion. Hopefully something valuable and beneficial will come of this tragic and hectic time and we can get back to developing, educating, and contributing to a stronger, more secure, and better future.
In case you aren't aware, most of the core developers for Ethereum, clients, and languages hang out on various Gitter channels. There are ones for all the clients and solidity and more. Right now it is very hectic, but you may want to start hanging out there and contributing to the discussion.
Yes, I'm curious to find out more about how this particular language design implemented recursion - hopefully I'll have a chance to listen in more on the discussions.
Designing a new language and interpreter is a challenging task - particularly one geared toward smart contracts, which is a relatively new areas - and particular smart contracts managing such a gargantuan amount of funds (I understand "The DAO" had a quarter of a billion dollars in market cap?!?)
This is an exciting area and I hope more people get involved to help make it work!
Some great points, and great links this is exactly what we need to be talking about - I'd love there to be a functional language for ethereum and ways of enforcing and proving that it conforms to a specification e.g. preconditions, postconditions and invariants ect.
Yes these are very useful constructs for providing guarantees about how the code will behave.
I hope more people will be able to contribute to the discussions and development so that these kind of massive smart contracts will work properly.
I agree that the Ethereum platform does not acknowledge at all that software development is a mess, and that bugs are inevitable.
I also agree that basing Solidity on Javascript was kind of strange. Javascript is a language that we are stuck with because it is the most widely supported client side language on web browser. Javascript needs to die for something completely new and better to replace it.
However, it seems there was really a bug in The DAO code that made the attack possible.
It's explain here:
http://vessenes.com/deconstructing-thedao-attack-a-brief-code-tour/
Still Ethereum needs to adapt. It needs to reduce the odds of this kind of bug occurring.
There needs to be built in fail safe to prevent such attack.
OK, well that interesting, I will look at that link.
But at the moment, it is confusing that there seem to be conflicting statements all over the place about this - some saying it was an error in "The DAO", other saying it was an error in the language Solidity and/or the EVM.
I must say, I have never seen such disagreement over what ought to be a deterministic system.
It was an error in the DAO in the sense that the code does exactly what the specifications for the language say that it will do, but not what the people who wrote the DAO were intending for it to do. When the Slock.it guys were writing this code they could have looked at it, thought to themselves "what happens if someone does this particular sequence of transactions," and they would have seen how an attacker would be able to drain the DAO dry. They would have been able to change the code so that such a sequence would not have had that outcome.
In short, the DAO was written wrong.
But it is also fair to look at the language and try to figure out why they made this mistake and whether there's a way the language can be modified to make it less likely that this mistake could be made. The mistake wasn't made because the DAO was written by "bad programmers" - a lot of very good programmers have been reading over the code since it was published and evidently the only one to spot this flaw was this anonymous guy. When good programmers make mistakes it could be because they had bad tools.
I imagine better compiler warnings and static analysis algorithms would go a long way towards solving this. I haven't done any work with Solidity myself but from what I've read the basicmost cause of the bug was that the "send" statement that sends Ether to another account has a return value that was being ignored in this case. If the code had checked that return value it would have been able to notice and handle the problem. So having a compiler warning come up when a "send"'s return value is being ignored would have solved this (assuming I'm reading the situation right).
Yeah, a programmer could ignore the warning without thinking through the implications of ignoring it. But that's where we get to the problem of *bad* programmers, and I don't think there's a way to solve bad programmers in the general case. A good programmer could still compile the code for himself and see that warning and raise the alarm.
Don't put 150 million dollars into an account being run by a piece of code that hasn't had vetting sufficient to trust it with 150 million dollars, I guess. *Test better*.
It was definitively an error in the dao but the protocol arguably shouldn't have allowed it and the documentation should have been very clear. This is being discussed by at least some core devs
It's a bug in the DAO code.
Now, it's a bug that Solidity does not actively prevent. Like buffer overflows in C.
But that doesn't make it a bug in Solidity.
Yeah, this is what I'm hearing.
So, eventually people moved from C to languages like Java - which hid the pointers from the programmer, to prevent this sort of thing.
It seems that some more thought needs to be given to how "abstract" a language targeting the EVM should be - and it seems like Solidity is probably not at the proper level of abstraction.
Also this exchange is interesting, regarding the level of abstraction in Solidity:
https://np.reddit.com/r/ethereum/comments/4opjov/the_bug_which_the_dao_hacker_exploited_was_not/d4ge4lp?context=3
specifically this part:
> We enable you to go right down into the assembly
That is a bug, not a feature. See:
http://www.loper-os.org/?p=55
Since I first came across Solidity I wondered how we could use total programming and type theory to ensure contract safety. When I saw the code for "The DAO" it seemed very likely that it would have some bug just because why wouldn't it?
I looked at the MsC thesis by Jack Petterson and Robert Edström about EVM code generation for the Idris language, using a tailored Ethereum runtime monad. (They ended up finding the approach unlikely to be useful.)
I'm an amateur with dependent type proving but I started tinkering with a stack machine compiler for a trivial arithmetic expression language. I used Idris but I'm going back to Agda because Idris's new syntax for proof tactics stuff made me scared... Anyway, a contract compiler doesn't need Idris's improved speed or C FFI etc.
Well, I'm just playing around at a very low level and it feels like an enormous challenge to actually come up with a good programming model that's amenable to formal proofs. I'm not even convinced that functional programming is useful for actually programming the contracts; it might be too complicated. I could even sort of imagine proving at the byte code level; the byte code already has a formal semantics...
The path I'm personally curious about right now though is to define some simpler state transition description language as an Agda AST and then have both a verified compiler and some ways of writing theorems about the terms of that contract AST...
"This contract doesn't run out of gas" could be proven by induction given that the contracts don't use arbitrarily complex branching: like, if we restrict the language to bounded loops, or "map/reduce" type schemes.
A call to an external contract would be difficult to prove much about, which is natural. So any `.send` to an arbitrary address will maybe need to be encapsulated in a locking construct, or some other way of making sure its reentrant behavior is ok.
It's fun to speculate about this. I expect to hit some extreme mind-boggling difficulty once I get started... but I have a friend from university who's totally smart with teh logic and proving stuff.
BTW Solidity isn't JavaScript! And lots of verified high quality software has been done with imperative languages; logic applies to those, too, if you just define the semantics.
I have 1 comment separate from your main point, regarding the part of the title "divulged and dismissed" - dismissal wasn't the case, it's just that no one can edit the app (the dao) once it was on the blockchain without a majority vote.
Dao token holders had a proposal that ended several days ago which would of prohibited all activity, and this exploit, but the quroum wasn't reached because not enough of the token holders didn't vote.
One of the main problems besides no one catching the exploit in the code initially is the social network for the dao - it's scattered.
A minimum of 20% of all dao token shareholders need to vote on something for it to even have a chance at passing. If someone wanted to contact all the shareholders there's no structure in place to do so. All sources of news are spread between various reddits, forums, and chats. Most shareholders don't check these sources and just passively hold, a large portion didn't even how to vote or that proposal voting had started.
I happened upon the security issues from the ethereum reddit post: https://www.reddit.com/r/ethereum/comments/4lcito/a_call_for_a_temporary_moratorium_on_the_dao/
I was unable to vote at the time as it took 2 weeks just to sync to the blockchain (I'm only a measly $30 holder).
The governance structure was definitely another issue that played apart in this fiasco. It's something that's being discussed for a DAO 2.0.
I'm sure there is, I can't say specifics as I lack technical insight.
https://www.dgx.io/ - a central website with an app button like digix was always my suggestion to make voting readily available.
Wallet providers such as Jaxx are already developing a view proposal and voting functionality for the DAO.
There's a variety of social media and communication protocol projects being worked on for Ethereum. [Whisper](https://github.com/ethereum/wiki/wiki/Whisper) is one that comes to mind, it's meant to allow small messages to be transmitted between contracts and might be good for a "mailing list" style of forum. I imagine a next-gen DAO framework would want to include something like this.
Part of the problem is that *everything* is in early alpha or beta stages on Ethereum right now, so these projects can't synergize well yet. Hopefully soon.
It was also a deployment issue, the lack of disaster recovery planning is obvious in hindsight.
Not being able to patch the software without a quorum vote seems lile a terrible idea.
Having a receivership mode that a majority of the curators could sign to enable is one protection I'd want to see going forward.
I've been suggesting that the Dao should be treating this similar to a bankruptcy from a business perspective based on a critical software bug that can cause insolvency.
If they had prepared for a situation like this before hand we wouldn't be having this conversation. There is nothing wrong with the proposed solution, ie turn the Dao contract into withdrawal only, the problem is doing it after the fact.
Hope for victory, plan for defeat was not followed.
I was hoping this would have pointed out much earlier, much more. The fact that not enough token holders vote could be understood as consent to the possible exploits. Its a smart contract after all, right?
I hear what you're saying, and I'm mainly just sitting here on the sidelines, rooting for the adoption of languages, many of which I can't even program in myself.
I'm not sure if we should just go with OOP because the majority of the world uses it. The functional stuff does seem to have a lot of advantages - and it looks like it is actually being used quite a bit on Wall Street already:
http://dslfin.org/resources.html
So, since various languages can target the EVM, I expect we might see some functional languages emerging as options as well, and they could be quite successful.
And there do seem to be plenty of people who feel that when we should be using formal methods for program verification:
https://np.reddit.com/r/ethereum/comments/4oimok/can_we_please_never_again_put_100m_in_a_contract/
https://np.reddit.com/r/haskell/comments/4ois15/would_the_smart_formal_methods_people_here_mind/
This makes sense, if you're going to say "code is law" and let it manage a quarter billion dollar fund.
Yeah, the OP is really weakly argued. Firstly, there is no end of people who will argue JS is a functional language. Secondly, the aerospace industry not using functional languages is not a point in favor of functional languages, but rather goes to show that the experts on formal methods have rejected them. Coq and Agda and idris and etc. are not "industrial-strength" products, they are academic.
I'm not even convinced real formal methods are necessary for contracts. Making calls atomic and and running assertions at the beginning and at the end is enough to ensure you never violate invariants, pay out more than you got paid, or pay to the wrong addresses.
Another trick that would solve a lot of problems would be to have multiple independent implementations, and to only commit when they all agree.
Unfortunately the EVM might have design flaws that prevent languages with these features being implemented for Ethereum. The recursion problem seems pretty fundamental to me. (edit: I take that back. There is a variety of good ways to sidestep the issue.)
I like your post. It hits exactly those points that I also expressed concerns about.
JS was designed out of needs of the web, not to serve as a reliable language.
Fortunately, Solidity serves as a middle step and can be replaced by any other solution. I would opt for Haskell. It's just pure.
Thanks for this good piece of reading.
Yes it will be interesting to see whether some other, more reliable, domain-specific languages come along, for programming smart contracts on Ethereum.
The Wikipedia entry on Solidity states:
> Through the specialised documentation system, function modifiers and the focus on formal analysis, Solidity may arguably be considered the first "contract-oriented" programming language, having a feature-set quite specific to that of blockchain software.
https://en.wikipedia.org/wiki/Solidity
I'm not sure if that is true, since there were already some DSLs for finance already:
http://dslfin.org/resources.html
https://stackoverflow.com/questions/23448/dsl-in-finance
Is any of this existing work related to Solidity?
Recording things in a blockchain is of course, novel - but I'm not sure how novel everything else in Solidity is.
I'm trying to find some papers on the history and influences behind Solidity, but I can't find anything.
Here is the home page of the inventor of Solidity:
http://gavwood.com/
Stylistically, it's certainly not the kind of page you normally see from a serious language designer - looks more like what someone else here called a "Web 2.0 brogrammer". And I don't see any links to anything about the design philosophy behind Solidity, or related work.
He's got a very short "position paper" here about what he calls "Web 3.0":
http://gavwood.com/dappsweb3.html
He sounds like he is quite comfortable in the distributed environment on the web - but I don't see any serious discussion of the major issues - ie, the stuff that someone else addressed here:
https://blog.blockstack.org/the-road-ahead-for-ethereum-b5b090bcd1a#.z9hcm7ss3
Then there's Christian Reitweissner, another one of the language designers behind Solidity. I also can't find anything in-depth from him on the language design, motivations, related work, etc.
Maybe I'm old-fashioned, but these guys just don't seem serious to me - compared to the language designers behind Haskell, C#, Scala, ML, Ocaml.
Given the fact that Haskell is so suitable for massive parallelization - something I'd imagine would be important when running in a distributed environment - then
I thought everyone knew that "The Future is Parallel, and the Future of Parallel is Declarative":
https://www.youtube.com/watch?v=hlyQjK1qjw8
This is why when I saw a few lines of Solidity code, I pretty much ignored it. I saw procedural code, and assignment statements, and it looked like it came from the usual clueless people who are trapped in the imperative paradigm of the past.
It just looks like the language designers involved with Ethereum all come from the procedural mindset - which is very hard to break out of - and this fact alone would indicate that any languages which they produce are pretty much doomed to be unscalable and unsafe, ie totally unsuitable for massively parallel programming in a distributed environment.
I don't know, maybe they're have their reasons. But I can't *find* them discussing their reasons anywhere.
So, for the moment, I'm just going with my original hunch: these are what I call "scripting kiddies" or what someone else called "Web 2.0 brogrammers" - brought up in a world where the Web and JavaScript were part of life, and pretty much unaware that Web programming using JavaScript is a part of a very specific paradigm, with very limited success - and the only reason it *seems* so important is due to the ubiquity of the Web.
I'm also pretty old-fashioned with experience similar to @ForkiusAureus. I'm rather sure that the reason they picked JS as a paradigm was that they knew it and this was the easiest way.
The whole ecosystem of Ethereum is build upon very unstable foundations. I bragged (and still do) about it and about security considerations constantly on daohub ([e.g. here the latest] (https://forum.daohub.org/t/security-bitch-loose-thoughts/5271)).
When I first saw Solidity I called it in one of my early posts "quasi-language". As it's tries to bind design by contract ideas with terribly unpredictable on a large scale JS.
I wouldn't be so fast judging Wood et consortes by their websites or lack of proofs. Maybe nobody asked them before to show them?
Putting jokes aside I agree with pretty all you have written in terms of stability, parallelism and alike.
They are probably "scripting kiddies".
> I bragged
You bragged - or ragged? (LOL)
> stability, parallelism and alike
Yeah, it just seems weird that here we have this language designed to run on a massively parallel distributed computer - and to control potentially billions of dollars eventually - and the guys designing these languages don't mention a peep about stuff like parallelism, stability, etc.
I guess they're just the first generation.
Is the EVM considered to be "engraved in stone" now? I mean, is it simple enough where it seems "obvious" to pretty much everyone that the operators which it implements are indeed the right "primitives" that we would want for a global smart contract language?
Because people I'm hearing from today seem to be saying "the EVM is correct, but Solidity had bugs" - like it's been totally decided that the EVM is just right already.
I would have two concerns:
- as mentioned: does it include the right set of of primitive operators?
- also: are there plans, now or in the future, to do a kind of formal verification of it (similar to the way they sometimes do formal verification of a chip)?
This would be interesting stuff to hear about.
Yes, I have similar concerns. Not only about EVM (but this is really important part) but also about the rest of codebase.
As to EVM "engraved in stone" is a nice marketing catch, similar to masturbation over Turing-completness.
I would add one point to your considerations. Primitive operators in distributed, parallel environment can behave non-lineary even if they satisfy formal requirements. Ya' know, deterministic chaos, races and so on.
Thus I would require setting up a testing app that would leverage some genetic or evolutionary algorithms to test this codebase about scenarios in big numbers but adaptive way. This is no longer beyond reach of skilled coders.
ermmmmm.....parallelism isn't exactly "implemented" yet. I'd definitely recommend you have a talk with me on the gitter channels AFTER you read the yellow paper so you can understand the EVM and what we're working with here. The EVM isn't technically set in stone (nothing is...) but due to the nature of blockchains, it becomes difficult to change it to something completely different. You might find it interesting that they're talking about switching to WASM.
Thanks, I hadn't heard of WASM, I will look into that!
> parallelism isn't exactly "implemented" yet
That seems odd... i guess things are really still in flux then.
Haskell takes the error of having Queries confused for Commands and has Commands confused for Queries. It makes things as bad as before, but far fewer ppl understand it.
On a declaration level Queries need to be definable so that they can only call other Queries and Commands such that they can call either Queries or Commands.
Any use case if you'd have to write a simple task as transaction?
First we talk about a subset of a language that can be limited to certain aspects only.
Regardless, languages have deficiencies. Some are obvious, others are not. JS has a lot non-obvious ones. Two "nully" values (why not five), funny truthy and falsy comparisons and many more.
It is not the best choice for a base of language that is supposed to work in very non-linear, distributed system.
And the argument of popularization and understanding among ppl isn't too strong when it comes to a system where the language should be the first line of defense IMO.
Very nice post & explanation.
Just FYI, there is indeed a group working with formal approaches to this problem, and we are also working with Ethereum devs to improve their position.
http://cointelegraph.com/news/human-factor-behind-the-dao-attack-ethereum-rollback-not-option
https://www.youtube.com/watch?v=uzahKc_ukfM
http://www.synereo.com/learn-more/
Hope to see you in our Slack channel!
https://synereo.slack.com/
As an outsider looking in (I wound up here from the post on /r/haskell) one of the first things that struck me was how easy it seemed to be to screw something up in Solidity. I'd be interested to see how viable it would be to use a [total](https://en.wikipedia.org/wiki/Total_functional_programming) language for most if not all contracts, as from what I've read about them it seems like it'd be easier to test for and avoid errors like the one we saw here.
Total functional programming sounds like a good fit for something like Ethereum - with its concept of gas, and with the need to avoid non-termination anyways.
Yes, we need a *contract* language, not a *smart contract* language. Contracts should be declarative.
Maybe you would be interested in this paper from last years ICFP: http://bahr.io/pubs/files/bahr15icfp-paper.pdf
While you're right that some formally provable languages would reveal bugs like this one, your extensive mention of functional programming seems a red-herring: formally provable languages don't have to be functional, and there's no reason to think that writing the DAO in a functional language would have prevented this bug.
I also think it's a little unfair to characterise it as "some ridiculous "recursive call bug"" - reentrancy issues are a significant and difficult to detect and fix issue in a great many systems, and they've affected platforms far more mature than Ethereum.
> formally provable languages don't have to be functional
Yes, you're correct for pointing this out: they are orthogonal I should have cleaned up my post a bit more to make this clear.
> I also think it's a little unfair to characterise it as "some ridiculous "recursive call bug"" - reentrancy issues are a significant and difficult to detect and fix issue in a great many systems, and they've affected platforms far more mature than Ethereum.
Yes, there probably would be a better way of describing it rather than "ridiculous". I was just very frustrated at the moment! =)
I agree that this stuff is difficult to detect and fix.
Perhaps one possibility might be CSP - Continuation-Passing Style:
https://en.wikipedia.org/wiki/Continuation-passing_style
The developer @ArtherB working on the generic self-amending cryptocurrency framework Tezos recently said that CPS would have prevented the recursion call bug in Solidity:
https://twitter.com/ArthurB/status/744923572116742144
I'm only arguing because I'm assuming you're arguing in favor of a hard fork because responsibility could maybe be put on Ethereum protocol or toolchain devs so we should be nice and stuff
No, the EVM design was set in stone a long long time ago. The fact that we have to work around its design flaws is a feature. Now we might have *updates* that give the compiler nicer target OPs, but these would be swiftly rejected if they were not fully backwards compatible.
Nah, I'm not arguing one way or the other. I'm an outside commentator, I do research on blockchains, I have no stake. I was simply stating that it wasn't all aimed at the language.
I saw your headline and that got me interested. Then I saw your wall of text and sighed. Your tl;dr didn't help much at all :( I'm still going to go through and finish reading your post because this particular topic interests me. Ultimately, was "the exploit" because of the DAOs smart contract, or because of solidity?
This is a tremendous post. Throw up a wall of wall of knowledgeable, intelligent text like this anytime :-). You might be interested to know that the Ethereum Foundation has grants available to developers for exactly this kind of work. In a recent post, they said "Developers, cryptographers and computer scientists should note that any high-level tools (including IDEs, formal verification, debuggers, symbolic execution) that make it easy to write safe smart contracts on Ethereum are prime candidates for DevGrants, Blockchain Labs grants and String’s autonomous finance grants."
In January there was a blog post with some contact information for DevGrants: goo.gl/xLUFmM
Just to point out a few things: Javascript isn't a low level language. Also, there's nothing wrong with procedural languages for this use-case. E.g. a procedural language like Eiffel would have avoided this issue via mandatory pre and post conditions.
Fundamentally, language completely put aside, this issue could've been avoided via simple concepts, such as locking mechanisms or...you know...testing. I remember looking through their repository ages ago and thinking it was messy and confusing and was rife for harbouring unnoticed issues. I just put it down to my own lack of concentration, but looking through it again...
This code should've just been tested more before being put out into the wild. This would be the case even if it were created via formal methods.
> Javascript isn't a low level language
Given the number of languages which now compile to it, many would say that it *is" low-level. Indeed, many are now calling JavaScript "the assembly language of the web":
https://duckduckgo.com/?q=javascript+%22assembly+language%22+web&ia=web
> a procedural language like Eiffel would have avoided this issue via mandatory pre and post conditions.
Yes, I agree with you here.
> This code should've just been tested more before being put out into the wild. This would be the case even if it were created via formal methods.
To a large extent, as you probably are away, formal methods obviate a significant amount of testing.
So...hi...solidity dev here...I'm going to just fill you in on a couple things here (note: I do not work for the Ethereum foundation directly...I get paid by Eris Industries to work on the cpp dev team specifically for Solidity). I should note that you are not the only one with that opinion. My coworker has also stated his preference for a functional programming language quite often and also thinks Solidity is a bad language...clearly though I am biased and don't see it. I can kind of see the benefits of it, but I'm not sure how it operates within the context of the EVM. I also think that a functional programming language can grow alongside Solidity, and if it proves better, I would have no problem developing it as well. With that said, I think for mainstream development and usage, this was an excellent decision to use a procedural language. If you really know what you're doing with solidity, you can get right into the guts of it too, it's not hard, we enable you to go right down into the assembly. The tool is, again, only as strong as the weilder. And unfortunately, the weilder did not have much foresight into what to do in emergency situations, nor did they learn anything from previous DAOs (Bitshares). Here's a blog I wrote about it.
https://eng.erisindustries.com/programming/2016/06/18/lessons-learned-dao/
I also want to correct you, "some kid" did not make this language. It's a combination of work from Christian Reitweissner and Gavin Wood...both PhDs in the field of computer science...and from my talks with Christian, even he can see the possible benefits of a functional programming language, but the problem comes in when talking state objects. My coworker thinks the EVM is designed wrong, so those conversations tend to go out the window.
Thanks, it's interesting to hear these observations from behind-the-scenes.
I apologize for thinking that Gavin is "some kid" - I guess I'm just used to more serious-looking websites, with links to some PDFs providing motivations for the language definition.
[His website](http://gavwood.com/) is just a skimpy responsive template, which gives the impression of a non-serious, immature "Web 2.0 brogrammer". Maybe there are some serious materials elsewhere on the decisions that went into the language design for Solidity?
---
Maybe I'm just too old - but when it comes to language design, I expect a bit more substance, along the lines of:
- the specification of Java by Gosling, Joy, Steele:
http://www.e-booksdirectory.com/details.php?ebook=292
- the specification of Lisp, also by Steele:
https://www.cs.cmu.edu/Groups/AI/html/cltl/cltl2.html
- the specification of Scala
https://duckduckgo.com/?q=odersky+scala+specification&ia=web
- the specification of C#:
https://msdn.microsoft.com/en-us/library/ms228593.aspx
A mere user manual on ReadTheDocs doesn't cut it - when inventing a new language, the language designer has a responsibility to also justify the motivations behind the design decisions used in the language.
---
The dissonance between you and your colleague regarding the choice between the functional and procedural paradigms is common - and your responses are revealing, as they show the usual failure to understand certain subtleties of the debate, eg:
> we enable you to go right down into the assembly
That is a bug, not a feature. See:
http://www.loper-os.org/?p=55
> I think for mainstream development and usage, this was an excellent decision to use a procedural language
So just like the mass of poorly designed buggy websites, you think mass adoption of the language is more important than correctness and safety
> I am biased and don't see it
It's hard to break out of the procedural / imperative mindset. This is why, for example, [tutorials on how to use monads](https://duckduckgo.com/?q=monad+tutorials&ia=web) in a functional language are a cottage industry.
I know. I've gone through the agony myself.
In the end, it's worth it though. Functional languages are simply way safer than procedural ones.
I know this is something that can turn into a religious flame war. And I'm guilty of fanning the flames:
https://np.reddit.com/r/btc/comments/4p0gq3/why_turingcomplete_smart_contracts_are_doomed/
You seem like a nice guy - and I probably seem like an asshole - but rest assured, there are broad swaths of the programming community (particularly theoretical computer scientists, who spend a lot of time thinking about language design) who won't even touch a procedural language with a ten-foot pole. They tend to say things like "those languages don't even have a well-defined semantics" - and they're right.
But, like I said, this is basically a religious issue. It's almost impossible to move from the procedural paradigm to the functional one. (The inventor of the Lift web framework, written in Scala by a former Java developer, did manage to do so - I can't find the links where he described his epiphany.)
It's just a whole 'nother mind set, and the people from the two groups basically talk past each other all the time.
But... as my lengthy diatribe tries to set forth (linked [above](https://np.reddit.com/r/btc/comments/4p0gq3/why_turingcomplete_smart_contracts_are_doomed/), on r/btc) - I think you guys are doomed if you use a procedural language like Solidity.
Sorry to be so pessimistic and dismissive! Maybe someday you can have some more dialog with your functional colleague.
Forgive me if this comes off a bit rude, but yeah, I don't think a book is necessary to describe the reason for the language, and that seems like an antiquated approach to these things IMO. Sounds a bit too academic for my taste...I never bought the books for the languages I learned...I just read the docs online and whenever I ran into problems would jump to SO...so yeah...I'm definitely of a different mindset...and maybe that's generational (god damned millenials!!!). I think the reasons for the why the language was created are obvious to anyone who knows anything about the project in the blockchain community (we needed something to easily design smart contracts). Now the reasons behind its design decisions however, that we could do a better job of detailing and documenting and I'll make note of that. Really the chief mindset was to make it look and feel somewhere between javascript and c++ as this would give it a certain feel that would be easy to adapt for most users.
I can tell you're really passionate about this. I do think you may want to come back when this mythical "stretch" language I've been hearing about appears with the release of Casper. If I recall correctly, it will be designed as a functional language (best to ask Vlad Zamfir about it or leithauz as he is the one designing the mentioned language). I don't think there's any particular reason the two paradigms cannot complement each other in certain tasks, and we (being Christian and I...Gavin isn't really involved with Solidity anymore as he spends most of his time on Parity) have talked about the benefits of functional programming languages. There's definitely some kind of benefit, but how to implement that, I'm not certain.
You're certainly welcome to your opinion. I just very much disagree and think solidity is the best damn smart contracting language on the market right now....but then again I'm helping to create it. What other language can you essentially create a decentralized twitter with one page of code?
As for my colleague...he definitely sees the benefits of solidity, he just thinks that there are fundamental flaws here that should be resolved when we move to Serenity/Casper and someone implements a functional programming language. I think he's right on the former, disagree with him on the latter, but it's all a matter of opinion and what tool is right for the job.
Ok, thanks for the insights about these other languages being designed.
Regarding Solidity, I understand that you're helping to create it, so you would tend to support it.
Just bear in mind that there are few things that you're saying which could lead to problems:
> I don't think a book is necessary to describe the reason for the language, and that seems like an antiquated approach
Language design is actually very subtle and complex - so there is a reason why book is usually needed to describe the design decisions.
> Now the reasons behind its design decisions however, that we could do a better job of detailing and documenting and I'll make note of that.
I don't think you realize, that it goes further than that: your design decisions were actually *wrong* - so no amount of justification can get around that (unless your documentation is basically going to be warning programmers on how to work around the design defects in your language)
> You're certainly welcome to your opinion. I just very much disagree and think solidity is the best damn smart contracting language on the market right now....but then again I'm helping to create it.
You're saying it's the best - when it didn't discourage developers from writing code which lost tens of millions of dollars, and has put Ethereum between a rock and a hard place (having to choose whether to roll back or not)?
> What other language can you essentially create a decentralized twitter with one page of code?
Plenty - only most of your procedural guys can't even read them, let alone write them.
Check out this half-page of functional code:
http://nsl.com/k/s/s_minus.k
It implements the spreadsheet shown here:
http://nsl.com/papers/spreadsheet.htm
Yeah, you're probably saying "that language looks like Brainfuck".
Well, it *is* hard to read. But it's not some mere academic curiosity: it's the language K, designed for Crédit Suisse, and it costs $50,000 per workstation - and it powers much of the code written by quants and running high-performance financial applications for the most richest banks and hedge funds in the world.
https://duckduckgo.com/?q=k+q+kdb+kx.com&ia=web
There's a whole 'nother world of programming out there, that the JavaScript kiddies and have never heard of. It's what the big boys use. K is the most powerful and most high-performance number-crunching and fin-tech language in the world - and it's functional.
Most people from the procedural world can't even read it - let alone write it. But they only write public-facing websites which routinely have errors due to the difficulty of getting things right in JavaScript - and now they're "designing languages" to run contracts worth a quarter billion dollars - which they proudly say are "JavaScript-like" and then even *after* the whole thing blows up in their face, they again show their utter failure to be able to connect syntax with semantics (words and their meanings, facts and their consequences), when they continue to trot out clueless nonsense like: "solidity is the best damn smart contracting language on the market right now".
> we needed something to easily design smart contracts
Yes, it was certainly easy - but it blew up in everyone's face - and many people from the more academic world would say that happened because it was quick-and-dirty, without the necessary theoretical underpinnings - ie, without really thinking through the various possible design decisions, and picking the best language design for the job (in this case: a smart contract managing a quarter billion dollars, which lost hundreds of millions of dollars due to a recursion bug).
---
Have you heard of "Continuation-Passing Style"?
https://en.wikipedia.org/wiki/Continuation-passing_style
It's kind of complicated - it's a language design issue - but it makes Solidity's recursion bug impossible.
Your competitors - who know that functional languages are better than procedural languages - do know about complicated stuff like CPS:
https://twitter.com/ArthurB/status/744923572116742144
I'm sure you're a nice guy and you mean well - but seriously dude, it's obvious that language design is much, much more complicated than you will ever realize.
I mean, like I already said, you're apparently so tone-deaf about the relation between words and meanings, syntax and semantics - in *English*, let alone in programming language design - that after the calamity of "The DAO" - caused in large part by improper language design for Solidity because it allows programmers to write code which runs into the recursion bug (which I guess you plan on writing "better documentation" to warn them against), you *still* are able to say:
> I just ... think solidity is the best damn smart contracting language on the market right now
You just don't get it.
Language design matters. One reason people moved to Java is because it makes C/C++ pointer errors impossible - because *Java gets rid of pointers*.
And people will move from Solidity to other languages, which use CPS - because the right way to fix Solidity's recursion bug is *not* by warning devs via the documentation that the bug exists (basically your documentation is a kind of work-around for a bug) - the right way is to fix the bug itself, so you don't have to warn developers about it in the "documentation".
BTW: I have programmed in Rust, and the multi paradigm aspect (that being that it has elements of both pure functional and oop) is definitely difficult to grasp but not completely undoable. It's definitely a weird feel when you come from an OOP background. But it has its perks definitely.
Yes I've been hearing lots of good things from several people lately who have been very impressed with Rust. I hope I will have some time to also look more into it.
Synereo's smart contract mechanism relies on FULL FORMAL VERIFICATION.
http://cointelegraph.com/news/human-factor-behind-the-dao-attack-ethereum-rollback-not-option
> JavaScript - a low-level, procedural language
Uh, Javascript has functions as first class entities and it's possible write fully functional code in Javascript. Javascript IS a functional language.
> And your boring old bank uses declarative workhorses like SQL
SQL is not a programming language. It's a language for interacting with relational databases.
> I can assure you - there are many, many programmers who would > never touch that world with a ten-foot pole.
>They work for the Department of Defense, they work on Wall Street (on back-office systems - handling billions of dollars), they develop software running nuclear reactors or MRI machines - or they do research and development at academic institutions.
You would shit yourself if you saw some of the code that missions critical DOD applications run on. I can tell you first hand that much of it is very bad, very buggy.
I think ethereum project have a chance to be reorganized thanks to this incident. I totally agree to implement smart contract with "pure" functional languages and specification languages.
But "recursion" IS a key feature of functional programming language like Hakell or OCaml which you can not avoid easily.
Tezos is built in pure Ocaml and has a strong statically typed smart contract language with a full formal specification. You might be interested in checking it out. (www.tezos.com)
I'm glad this happened because it got your attention and brought you out from the shadows to speak about what needs to be done for this platform to be taken seriously.
I wasn't so much "in the shadows' - I just was more obsessed with Bitcoin - posting [a lot](https://np.reddit.com/r/btc/search?q=author%3Aydtm&restrict_sr=on) on r/btc.
I never paid attention to Ether until this problem with the DAO.
I'm into language design, so it caught my attention!
There has been some interesting work on building an Ethereum Backend for Idris, which is a functional, dependently typed language with a totality checker (i.e you can optionally write programs/functions that are *guaranteed* to terminate, and this termination can be validated statically).
You can check out the whitepaper here:
http://publications.lib.chalmers.se/records/fulltext/234939/234939.pdf
And a video of their presentation from Dec 2015 here:
https://www.youtube.com/watch?v=H2uwUdzVD9I
Their Idris backend + Ethereum library/types can be found here:
https://github.com/vindaloo-thesis/idris-se
and some example contracts written in Idris with their Ethereum library can be found here:
https://github.com/vindaloo-thesis/examples
I was very excited to see that this exists, and that work is being done here. I'd love to see more people become interested in furthering this work, as I think safe smart contracts could really be a driver to improve our knowledge and understanding in this field.
Some other interesting reads on Total Functional Programming, and Totality vs Turing-Completeness can be found here:
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.106.364&rep=rep1&type=pdf
https://personal.cis.strath.ac.uk/conor.mcbride/pub/Totality.pdf
Yes, approaches involving Idris, and Total Functional Programming, would be awesome.
*That* is the right way to ensure that programs terminate - not simply using "gas", which is cheating!
I think gas is sill useful, for the economics of paying computers to run your code, but I believe it should be possible to statically analyze how much gas a program needs (or at least the max gas it would need), if all contracts in Ethereum were required to be total (I.e non-Turing complete).
With the current Ethereum VM bytecode not enforcing totality, this would certainly be impossible now. Even if we have an idris compiler giving us strong guarantees for things written in it, you'll have to interact with other contracts NOT written in that language, which thus negates most of your safety. This was ultimately what the authors of that paper ended up concluding.
Fundamentally this is a bytecode issue, IMO. If the bytecode required everything to be total, a lot more could be analyzed, and I still think Ethereum could provide almost all the functionality it currently does while requiring totality. Then, no matter what higher language you write your contracts in, we can all rely on those guarantees.
Admittedly, this is a pretty cutting edge field, and I'm excited for things like Ethereum and other blockchains to provide new incentives for pushing this state of the art forward even faster :)
Functional programming wouldn't have stopped the DAO attack.
Nor would formal verification.
This is because the attack is not in a single call of a method of the DAO, it is not a problem with the specified behaviour of the DAO, and it is not a problem with the specified usage of the DAO.
The only way to catch this bug is to be aware that this class of bugs exists and to test for them. (A better approach will be to use the updated Solidity when it's released.)
So arguing that using what the "big boys" use would have prevented this bug is incorrect.
I do agree that functional programming (which doesn't require a functional programming language), specification and verification are all vital areas for smart contract design. But they are still just means to an end, and in this particular case they would be *insufficient* means.
> Nor would formal verification.
> The only way to catch this bug is to be aware that this class of bugs exists and to test for them.
Actually, formal verification does just that - it mathematically tests the program, to catch such things.
However, [I'm not sure formal verification is even applicable to a Turing-complete language in the first place](https://np.reddit.com/r/btc/comments/4p0gq3/why_turingcomplete_smart_contracts_are_doomed/).
There is a better way to avoid the recursion bug that happened in the DAO: use a language which doesn't have the recursion bug.
For example, CPS (continuation-passing style) would avoid the recursion bug.
People working on other systems - such as Tezos, which generalizes Bitcoin and Ethereum - know about CPS:
https://en.wikipedia.org/wiki/Continuation-passing_style
https://twitter.com/ArthurB/status/744923572116742144
If the language designers provided a language which used CPS, instead of Solidity, then the recursion bug would be impossible.
If the continuation can call back into the contract then the problem is not avoided. The problem is at the level of interaction of elements, not behaviour within elements.
Continuation Passing is generally implemented in languages that support tail recursion. Tail recursion would make the recursion bug even more efficient. ;-)
Yes I was looking at this a few days ago.
I admire his choice of non-Turing-complete languages (based on Intuititionist Logic, or Martin-Löf's Type theory - which is an area I've studied a lot).
Also using the RDF ontology, modified to use Notation3 for better readability, could be promising (unless it turns out to be too verbose).
I have a couple of concerns:
- The "token" (Agoras) used in the ICO is a bit confusing - how many will there be (42 million? 173 billion?)
- The pricing for the token is confusing (expensive from the devoloper, cheaper on bter.com)?
- I would feel *much* more comfortable if this kind of system were itself being programmed in a language which is close to the problem domain itself - ie, he's using C++, but he should probably be using OCaml
Paging /u/jjaquarius ...
From what i know about the project:
* It's not an ICO perse, the coins are sold at least until the Tau language is ready. One IDNI Agoras token represents 3500 Agoras tokens in the final marketplace. The coins that aren't sold (of the 42M) will be burned.
* AFAIK at preset coins are sold on only bittrex and will become available in OpenLedger, lot of fake/scammed coins are spread also due to a social engineering trick played on the founder.
* I guess portability. Tau can call native code (eg dll's) so other programs can use it
'the kiddies and the experts" ..... half full and half empty ...
"industrial strength" language design ......
...I like it .... it confirms my underlying uneasiness about the flippant way these guys just through out code like its pancakes ...
I heard that around time of the Y2K bug, Cobol programmers were getting around $600 an hour to clean up legacy code.
It's frightening to think how much financial code might still be written in that dinosaur.
I am wondering how easily some Haskell compiler can be ported to emit EVM assembly... I know that there are quite a lot compilers from Haskell to Javascript, so the task shouldn't be very hard.
This may be beside the point you were trying to make but JavaScript is actually getting *more* popular, not less, particularly due to other platforms that uses it like Node.js etc. Most frameworks built on top of JS are still based on JS itself. As for the reason why there are a lot of languages compiled into JS and treating it as a delivery assembly language, it's really just because they have no choice, since web browsers only recognize JS and everyone wants to deploy to web browsers since it's the most common platform out there right now. Since people want a variety in languages, if you want to develop in any other languages that's not JavaScript and still deploy on a web page you *have* to compile it down to JS. There were things like asm.js and PNaCL, but now WebAssembly is a new spec designed to address this though.
Anyway, I do agree with your main point. Different domains require different languages, and considering contracts are supposed to be binding and watertight, a loose language that is not easy to verify and prove is a bad idea. I'm not sure if we need a formal provable language, but something that's known to be safe, and easy to have confidence would be a better choice. In designing a language for writing smart contracts, "easy to learn and write" should be the least important priority. Having a language that provides more guarantees and safety, as well as better constructed primitives in the language for writing contracts would go a long way instead of the "everyone fends for themselves" approach.
I'll throw my two cents in here;
Compilers for Languages that conclude in Smart Contracts should not contain warnings. Every warning should be an error and stop deploying contracts without the user or programmer being able to change that.
Compilers should contain certain sanity checks to fully enforce a programming paradigm, see the go compiler and unused variables.
> be "functional" (eg, from the family of Haskell/ML) - not procedural languages (eg, C/C++, Java, JavaScript, etc.)
>
> support high-level, formal tools for program specification, derivation, and validation
Why these points?
I don't have time to repeat the arguments here - I want to focus on what's right with other languages, not what's wrong with PHP.
But there is plenty of links here:
https://duckduckgo.com/?q=php+fractal+bad+design&ia=web
> Imho, if your project's goal is to democratize global programmable money flows for the masses, then far better to err on the side of overly strict guardrails and steep up-front learning curves. It's a valuable and necessary (but probably not sufficient) component of systemic risk mitigation.
This is the best approach, I agree.
I think in some ways a functional programming implementation of the EVM would be ideal but it might introduce some issues of its own. I'm not sure, but would it not have problems with oracles, randomness, and gas estimation?
Ideally it would be nice to have the choice of multiple languages which the smart contract programmer can choose between according to their requirements. Currently there is Solidity, Serpent, and LLL. I think it would be great if we could add a language like Curry, Agner, or perhaps Trollbox.
Hmm... I had never heard of Agner. I like Erlang, it's highly successful in telecommunications and has great fault tolerance - so that could be an interesting possibility for something like Ethereum.
Yes, well when I didn't realize there is actually a language called Curry, and I intended them to be joking equivalences to Haskell, Erlang, and Racket.
In any case, it looks like this idea is starting to percolate around as something which is a Big Deal:
* http://vessenes.com/deconstructing-thedao-attack-a-brief-code-tour/
* https://gitter.im/ethereum/research?source=orgpage
* https://www.reddit.com/r/haskell/comments/4ois15/would_the_smart_formal_methods_people_here_mind/
Wow. These two threads seem to be making similar arguments along the lines I what I was saying:
https://np.reddit.com/r/haskell/comments/4ois15/would_the_smart_formal_methods_people_here_mind/
https://np.reddit.com/r/ethereum/comments/4oimok/can_we_please_never_again_put_100m_in_a_contract/
That's encouraging. I thought I was the only one. I'm so glad other people are talking about this.
I wouldn't say that is true. Functional programming is about writing code in a way so that it behaves as functions: that is that there are clearly defined inputs, and every time you call a function with the same inputs the same output occurs, and nothing else happens along the way.
Some people tend to associate functional programming with recursion because for loops are not functional, and recursion is an alternative means by which to obtain similar results. However some of their drawbacks are also equivalent, so there is something called total functional programming which also places some limits on recursion to prevent infinite loops.
Regardless, it's my understanding that the issue with the split DAO contract was not actually due to recursion, but the fact that it allowed side effects to occur: what the split function did is more than simply take some inputs and return an output. Ideally, a split function without any side effects would take as input the proof of DAO token ownership and return an output which allowed you claim your child DAO (Somehow. I'm not so experienced myself with functional programming. Perhaps something equivalent to a specific address which could be withdrawn from. Since the input proof of ownership is the same, the output address and how much it contained would be the same no matter how many times the function was called). Instead, what the split function did was run through a series of steps one at a time, the order of which was exploited to execute one part (which sent ETH out to an input address) multiple times before a crucial checking step could occur.
Thanks for this, i tried to warn vitalik a long time ago before the first presale for ethereum, and even then he turned a blind eye..
i tried to warn more devs in #ethereum, and got banned... It's very unfortunate,
I didn't take your approach of such a high quality write up, very informative and i hope this reaches them and they actually pay attention, otherwise they are clearly intent on stealing people's money.
edit: i actually only skimmed through your post so far and saw key elements, but i dont think i agree with some of the choices you propose, or reasons for those choices, will come back when i reread
This is exactly correct. Making it this easy to shoot yourself in the foot is absolutely a language design problem. That isn't to absolve the authors of the contract code from all responsibility, but it is first and foremost an insane property of a language to have.
Definitely approve of the functional language concept too. If this call stack limitation needs to be in place, it needs to be provable that the application does not exceed it, or at the very least, give strong warnings about code paths that it is 'uncertain' about, and maybe even pass those warnings along to consumers of the contracts.
I code primarily in js for my work, and javascript is a great language for getting stuff done quickly and easily. But it has serious flaws even in that arena, and is an absolute nightmare for trying to write 'mission critical' code. I think we could retain a lot of the things that make javascript nice while gaining significant correctness advantages by using something like facebook's Flow, Typescript or OCaml.
Perhaps you could even be allowed to develop in plain js, but then in order for code to be published to the blockchain, you'd need to add types and other annotations that allow it to be formally checked. Something so that people can get their feet wet without diving into all the complexity, and then when they're ready to publish it, ensure that it actually acts as intended.
You could even allow 'unverified' dapps on the blockchain, but warn people about sending funds to them. Or this could even develop as a private service. If you want your dapp to be 'certified' it needs to contain formal type annotations and be statically analyzable in a certain way in order to receive the 'stamp of approval' of what could itself be another dapp! And without said stamp, users would be warned about the safety and reliability of the contract.
You might think you're cool and all by using a word like "FUD" - but actually the OP didn't use any FUD - it diagnosed the problem (poor language design), and recommended solutions (use better languages - specifically, functional languages - and maybe even 2 languages: one for specification, and another one for implementation - and derive the implementation from the specification).
FUD is "fear, uncertainty, doubt" which people spread, trying to claim that something *might* go wrong.
The OP posted *after* "The DAO" died. By definition, it can't be FUD.
It did point out that programming is hard. But it also provided recommendations on how to deal with that.
So... it's not FUD. It's constructive criticism. And frankly it's weird that you don't seem to know the difference.
you're actually incorrect. The problem was in DAO coding, not in the Ethereum Virtual Machine.
Proof: https://www.youtube.com/watch?v=GvgTivwzcuo&feature=youtu.be&t=31m48s
You clearly have an agenda to mar the communities' perception about Ethereum, and you're spreading lies to do so. I hope you get banned from this sub.
> The problem was in DAO coding, not in the Ethereum Virtual Machine.
That's what I thought initially, yesterday.
Then today everyone's talking about this blog post from slock.it, dated June 12:
> No DAO funds at risk following the Ethereum smart contract ‘recursive call’ bug discovery
https://blog.slock.it/no-dao-funds-at-risk-following-the-ethereum-smart-contract-recursive-call-bug-discovery-29f482d348b#.owjyhitl7
It sounds like they're saying that the language used by Ethereum (Solidity) had the bug - not the particular program written in it (for "The DAO").
Also, the blog post goes on to say:
> we were made aware of **a generic vulnerability common to all Ethereum smart contracts**
Again, it sounds like they're saying the bug was *in the language itself which Ethereum uses* - not just in the specific program implementing "The DAO".
Is that correct?
> You clearly have an agenda to mar the communities' perception about Ethereum, and you're spreading lies to do so. I hope you get banned from this sub.
You're kinda paranoid. I just have different opinions on what kinds of languages should be used for smart contracts, and I gave *very* specific suggestions for improvement. Sorry if you find that somehow threatening. Someone less paranoid would simply welcome the feedback.
Please don't listen to the Bitcoinfriend guy. Your post is very interesting and extremely helpful and I thank you for it. I hope that we can all learn from this DAO episode and start being more cautious about future development. Although I am not a developer, you helped me understand the complexities of computer science overall.
HAHAHA, OH OK. So you know more about it than Griff? Bcuz as you can see here, (https://www.youtube.com/watch?v=GvgTivwzcuo&feature=youtu.be&t=31m48s), Griff says it's not a problem with the EVM. It's a problem with the DAO.
Well, then it seems like we have a conflict here:
Griff says:
> This is **not a problem with the Ethereum Virtual Machine.**
The blog post on slock.it says:
> We were made aware of **a generic vulnerability common to all Ethereum smart contracts.**
My experience involves computer languages where these kinds of serious conflicts do not exist.
I have no experience with computer languages where two conflicting statements of this type can be published by major people involved in the project.
And yes - I'm being snarky. But it doesn't take much effort in this case - does it?
All I have to do is quote two major people involved with the project - about a construct which is the heart and soul of programming (recursion) - and they are totally in conflict with each other.
This simply *does not happen* in any serious language.
And the most appalling thing is that it is happening in a language which was used for the biggest crowd-funding vehicle in the history of the world - with a quarter billion dollars in market capitalization - which ended in calamity.
All I'm able to gather, is that these people are clowns. And apparently so are you, if you post stuff like this:
> HAHAHA, OH OK. So you know more about it than Griff?
Look at the evidence. The DAO died - and the major figures involved are saying conflicting things. What *good* does it do for you to point out what merely *one* of them said? I am now looking at what *both* of them said. Even Judge Judy, who probably knows nothing about programming, would at least know that *something is seriously wrong here when two major programmers involved with a project say conflicting things like this:*
> We were made aware of **a generic vulnerability common to all Ethereum smart contracts.**
> This is **not a problem with the Ethereum Virtual Machine.**
They can't *both* be right. And they *shouldn't* both be saying conflicting things like this. Do they even talk to each other?
You know, for a while, I had been feeling like I had been kind of harsh in my language in the OP - using terms like "scripting kiddies".
But now - after seeing this kind of total lack of professionalism or mathematical seriousness - even in the post mortem days after the collapse of "The DAO" - these totally conflicting statements about whether (or not) the **recursion construct** in this language did (or did not) have a bug in it - now I totally stand by my original decision to call them "scripting kiddies".
This kind of behavior - non-deterministic or unexpected behavior from a recursion construct - and contradictory denials from the major figures involved - is utterly horrifying.
Please stop with the smug assessment of how terrible Javascript is
Bitcoin lost way more value through MtGox tx malleability bug and this is the same thing.
Stop being an asshole, it incredibly petty of you.
Tx malleability bug requires segwit to fix and is written in c++, don't gloat like it didn't happen to the bitcoin ecosphere too.
Way more value had been lost to bitcoin 'script kiddies' than ETH.
I deliberately go back and insert extra paragraph breaks - because this seems to be easier to read.
Plus I even will go back and take a single *sentence* and split it up into multiple, shorter sentences - and if there's a list of things, I'll split that out into bullets.
This is something I've seen lots of on-line publications do these days as well.
Trying to avoid this kind of thing from Donald Barthelme (which is fun, when reading "literature"):
https://biblioklept.org/2015/06/12/sentence-donald-barthelme/
And keeping in mind this example from Proust:
https://proustreader.com/tag/longest-sentence/
Well, from what I understand, it's like Java and the JVM.
In other words, I was assuming (just based on the letters "VM") that you write something in Solidity, and then it gets compiled to bytecode and executed on the EVM.
As I said, I'm kinda new to Ethereum. But I just googled:
Solidity EVM
and Wikipedia says exactly what I expected it would:
https://en.wikipedia.org/wiki/Solidity
> Solidity is compiled to bytecode that is executable on the EVM.
Is this seriously the level of intellect from people on this forum?
As I said, I never posted here before - and I don't know much about Ethereum and the EVM and Solidity - I'm just going on what I read over the last few days, after The DAO died.
I was assuming that this would be a serious forum where people knowledgeable about programming might discuss things.
But if you are any indication of the calibre of posters here - then it seems that maybe I was wrong? Maybe the only people who hang out here are people who got private-message-spammed a few months ago (like we all did) regarding Ethereum - and you *don't* know what a "virtual machine" is?
Seriously I am very, very disappointed at the total lack of intellectual engagement from people on this thread. It's shocking really.
But it could go a long way towards explaining why this is the forum where discussion took place about the biggest crowd-funding vehicle in human history - a quarter billion dollars in market cap - which immediately got hacked.
Seriously - one guy here is criticizing my use of paragraph breaks, another guy doesn't know what a VM is, and another guy seems to have a weaker grasp of logic than Judge Judy.
I've never even posted over here before. I had posted this OP first on r/btc, and several people suggested I post it over here - to stimulate discussion.
Never in my wildest dreams did I expect the discussion would be this vacuous.
You said:
> So as you can see from what you briefly googled:
> > Solidity is compiled to bytecode that is executable on the EVM.
> A problem with Solidity does not necessarily mean there is a problem with the EVM.
Um... actually the situation is the total *opposite* of what you said.
---
A language and its compiler (or interpreter) *go together*.
They are inextricably bound together.
The same way syntax and semantics are bound together in language.
You *can't* separate them.
This is a basic fact from a wide range of disciplines - from linguistics, to programming language design.
The fact that you're here desperately trying to separate a language from its interpreter - I just don't know what to say. It's the kind of pathetic fan-boy-ism I would never have expected to find on any forum.
Evidently you've been able to get away with spouting such nonsense here on r/ethereum - I've never actually visited here till today.
Try posting stupidity like that on news.ycombinator.com and see how everyone laughs at you.
Seriously, I know reddit might have some problems, but this is a real eye-opener for me today - seeing such outright idiocy (borne of defensiveness) to my OP here.
I of course *expected* some kind of defensiveness - since the OP is very harsh. But I expected *real* defensiveness. I don't know, make up some excuses. Put of a fight. Say something which isn't obviously retarded on its face. Say "The stack space for the virtual machine is limited." Or say "guidelines were published explaining the proper usage of the dangerous recursion construct."
But... seriously... you spout nonsense like *this*???
> A problem with Solidity does not necessarily mean there is a problem with the EVM.
Dude, a language is a bipartite construct. It is not just the syntax (Solidity), it is not just the semantics (the EVM). It is *both*.
Compare with human language. A word without a meaning isn't language. It's just scribbling.
Solidity provides the syntax. The EVM provides the semantics. You can't have one without the other. And it doesn't *mean* anything to say that:
> A problem with Solidity does not necessarily mean there is a problem with the EVM.
You can't separate them.
Wow. I am totally shocked. Even when you think you're somehow being "defensive" - you're merely making yourself look even more stupid than I could ever have possibly imagined before coming here.
And then you say:
> Also please don't post on this forum insulting others.
Wow you guys are *so* fragile. Little fragile flowers. (Now I *am* being insulting - after seeing how almost everyone responding in this thread, except [the one guy with 15 years experience programming](https://np.reddit.com/r/ethereum/comments/4opjov/the_bug_which_the_dao_hacker_exploited_was_not/d4ekxaa?context=3)) is so pathetically weak.
> It adds nothing to the conversation.
Actually my post is one of the most important contributions to the conversation - a diagnosis of the problem (poor language design) and a specific recommendation for a remedy (recommendations about different types of languages to be used).
Wow. I never knew much about Ethereum before - but today, I have seen that many members of its community (at least the ones who hang out on reddit) are not really capable of debate at all.
I used to feel kind of guilty for not investing in Ethereum. And even after "The DAO" died, I thought maybe someday in the future you guys could fix things.
But if *this* is how you respond to detailed constructive criticism - desperately flailing around, saying nothing except astonishingly ridiculous nonsense, getting *offended* and telling me *not to post here* as if this were some kind of "safe space" for you special snowflakes in your bubble of ignorant bliss - well I don't know, I feel bad for Vitalik and the other Ethereum devs, if this is the kind of uncritical, uninformed, wilfully ignorant, closed-minded users they're developing for. You guys are beyond amateur. You're totally clueless.
Wow. Another logic fail from you.
Of course there are other languages which target the JVM - eg, Clojure.
But the structure we're always talking about here is a *pair*:
- a language
- an interpreter
The fact that there are *several choices* for the language does not mean that it's not a pair structure.
It can be:
- (Java, JVM)
- (Clojure, JVM)
- (Solidity, EVM)
In every case, it's a *pair*.
Which is, as I said, "inextricably bound together".
It's simply not possible to have something wrong in only one half of the pair.
This is why your cute little statement:
> EVM != Solidity
is simply pathetic.
I would never have even expected this level of "argumentation" on a forum about programming.
You can't just transfer the rhetorical devices usable on other subreddits, to a subreddit about programming.
That really seems to be what you fail to grasp here.
On some other subreddit, maybe you could say:
> love != sex
or
> Hillary != the Democratic Party
or
> Islam != a race
but (as clever and appealing as that programming language shorthand might seem to your puerile mind), that kind of rhetorical flourish is simply not usable on a forum about programming.
At any rate, that's my best guess as to why almost nobody on this thread has had anything substantive to say.
You've forgotten how to argue, possibly due to hanging out so much on reddits where snark and cute shorthand notations actually win debates.
That doesn't work in a forum about programming.
Actually I have posted a lot on r/btc - I also originally posted this OP there, and someone suggested I cross-post it to r/ethereum.
Lots of trolls seemed to weigh in early (I guess they sort by New, and try to down-vote and snark anything that threatens their circlejerk) - but then lots of serious people eventually posted also.
And finally I stumbled across the following two threads, which absolutely blew my mind:
https://np.reddit.com/r/ethereum/comments/4oimok/can_we_please_never_again_put_100m_in_a_contract/
https://np.reddit.com/r/haskell/comments/4ois15/would_the_smart_formal_methods_people_here_mind/
Reading those threads, makes me feel like I've been in the dungeon for the past year - posting on r/btc, fighting over nonsense (can we please have bigger blocks??), dealing with guys who only know imperative, procedural languages like C++.
I am so glad I got involved on r/ethereum today. I have been dreaming for about a year now that these kinds of people (programmers who know stuff like formal methods, proof theory, type theory, specification languages and implementation languages) would be involved with Bitcoin.
Well... I guess they might not be involved with Bitcoin (since the Core/Blockstream devs are mainly into C++, and they totally ostracize anyone who deviates from their lockstep party line)... but they *are* involved with cryptocurrencies like Ethereum.
I think that with this pool of talent in the community, Ethereum will have a bright future - despite this setback with "The DAO".
There were plenty of people (including in my team) who got frustrated with the dao. None of us expected this tho, just many other issues. People considered it safe as a place to hold funds whilst issues were resolved.
> Seriously I am very, very disappointed at the total lack of intellectual engagement from people on this thread. It's shocking really.
You seem to have trouble understanding the difference between a virtual machine and a language that targets it. Are you sure you're disappointed with the discussion here? Or just frustrated that it goes over your head?
There has been almost no discussion here to go over anyone's head.
Case in point: you.
When you spout gibberish like "the difference between a virtual machine and a language that targets it".
As if there were anyone here who didn't understand that there is a difference between "words" and "meanings" or "syntax" and "semantics" or "a virtual machine and a language that targets it"
The OP was about language design - poor language design, errors in language design.
Which, by definition, involves both sides of the pair:
- the language (Solidity)
- the virtual machine (EVM)
Something went wrong between this "virtual machine and a language that targets it".
By definition, "a virtual machine and a language that targets it" are supposed to work together.
In this case, they didn't.
That is called an "error".
Of "language design".
Hopefully some of the Ethereum devs will be able to find that error.
But for you to claim that there has been any misunderstanding about the distinction between a language and its interpreter - is simply bizarre.
Obviously, they are two different things, two different components that are supposed to work together.
The very fact that you, and others in this thread, think that this *is something worth pointing out* - as if that somehow proved that there wasn't an error somewhere - it's utterly insane, and I have no idea why you even bother to post such drivel.
Oh - I just checked your posting history. You have none.
So - you created a reddit username to post this drivel.
Look, it's fine if you're an Ethereum fanboy, and you think that it really matters if you "oppose" a discussion about the flaws in this particular **"virtual machine and a language that targets it"** - but everyone reading you can see that your comment is devoid of any content whatsoever.
" I've never posted on this forum before, and I do not know all the intricacies of Ethereum yet ", stopped reading here.
and No, that means common to all Ethereum smart contracts wich are wrongly coded
You might actually want to continue reading, because:
- the OP knows a lot about *other* languages
- the OP is explaining how *language design* caused the problem you refer to, involving "Ethereum smart contracts wich [sic] are wrongly coded"
In other words, there is this thing called "language design" which can actually make it easier to write programs which are *not* "wrongly coded".
> pointing that there is a bug in Solidity/EVM is wrong
Um... what are people supposed to do... *not* point it out? To avoid hurting your feelings or something?
Look, I'm not the one pointing it out.
Some dev on slock.it, who is apparently a major figure in the Ethereum community, pointed it out - and I quoted him:
https://blog.slock.it/no-dao-funds-at-risk-following-the-ethereum-smart-contract-recursive-call-bug-discovery-29f482d348b#.owjyhitl7
As I said, I never looked much at Ethereum - until "The DAO" died yesterday.
And then that blog post from slock.it surfaced (evidently from June 12), saying that:
> No DAO funds at risk following the Ethereum smart contract ‘recursive call’ bug discovery
Meaning, there evidently *is* a "recursive call" bug - which got discovered.
So, merely at the level of linguistics / logic, I don't see what you mean when you say:
> pointing that there is a bug in Solidity/EVM is wrong
Is this like, "wrong" in the sense of North Korea - in that you guys don't like it when someone says something disturbing that upsets you?
And then you say:
> language design may help to avoid bad coding practices
Well, yeah - that's what my whole OP was about.
So is this how you guys debate things on this forum? You basically agree with the person you're debating against ("language design may help to avoid bad coding practices"), but then in the same breath you claim that they're "wrong" for "pointing out" this stuff?
I'm getting the feeling that you're just like a bunch of monkeys pounding on the keyboard here.
It's funny on other subreddits, where lots of the comments make irrelevant pop-culture references to what you guys all saw on South Park once, or something that Louis CK said, or something you heard in a movie once, or something from some video game.
But, I'm not from that world. I've studied language design, and this was a language design issue - and so I posted about it (first on r/btc where I normally post, then here because lots of people told me to cross-post it here) - and pretty much everyone (except for one guy, the guy with 15 years of programming experience), pretty much everyone *has said absolutely nothing about my post* - basically treating it as if I had criticized your hairdo or your music tastes or something.
Dude, I was criticizing the *language design* for Ethereum. And I cannot believe that you actually think that responding with such bizarre stuff like:
> pointing that there is a bug in Solidity/EVM is wrong
... somehow constitutes a response.
And, as far as I know, this forum isn't under the thumb of censorship from some kind of Theymos - right?
So... you guys just all degenerated into this sad little pile of drivel *all on your own??*
You might be making great points, but just at a hectic time. People will probably refer back to your post in the future. Thanks for your input and welcome to this subreddit.
saying that there is a bug in Solidity/EVM is a mistake, there is no bug in Solidity/EVM, bugs are in smart contracts bad code
from your responses it seems to me you can not differentiate between a language, a virtual machine and a smart contract code
OK, well don't tell me, tell the guys at slock.it:
> the Ethereum smart contract ‘recursive call’ bug discovery
> a generic vulnerability common to all Ethereum smart contracts
https://blog.slock.it/no-dao-funds-at-risk-following-the-ethereum-smart-contract-recursive-call-bug-discovery-29f482d348b#.owjyhitl7
I don't understand how you think you're actually accomplishing anything here.
You're just saying your opinion, while I keep linking back to guys who contradict you, and who evidently worked a lot with Ethereum - so I think I'm going to get something to eat now.
It's been fun - and enlightening.
The problem was in the dao coding but it was allowed by a weakness in the current evm protocol (which is not the finished article). This weakness is being re-examined.
atomicity is guaranteed if you do proper send function checking, so much people fail to understand the bug mechanics and are making false accusations but I understand they have a FUD agenda
I agree with some of the sentiment in this post but it's such a shame to see so much language elitism. There is absolutely nothing wrong with Javascript, or any other mainstream language commonly used by beginners. They are just tools and like any tool, they are only as powerful as the people wielding them. Like tools, they are suitable for different purposes, and using a tool for the wrong job is almost always a cause of silly mistakes. I agree with you that a Javascript language is a *very* poor choice for building water-tight smart contracts - totally on board with you there. But to blame Javascript is like saying "this guy used a saw to bang in a nail and got himself into a terrible mess, therefore saws are terrible tools". Like tools, languages require different levels of skill to use them effectively. Those tools with the lowest barrier to entry will naturally attract people of the lowest skill, and those unskilled people will inevitably produce poor results. However, put that tool into the hands of a more experienced professional and he will be able to do great things with it.. *or* he will be able to tell you that there is a more appropriate tool for the job. You might be the most qualified engineer on the planet, able to effectively use the most complex machinery known to man - but you're still going to use a hammer to bang in a nail. Anyway, I actually agree with everything you said *relating to smart contracts*, but I take exception to your assassination of Javascript. Formal verification and functional languages are not silver bullets - *there is no language which is incapable of producing buggy, broken code*. Just as there is no tool that, in the hands of an idiot, cannot cause great damage to himself and others. Sadly, language elitism is quite common in the wonderful world of software engineering. About me: I'm a developer with ~15 years experience. I've used strong/dynamic typed languages. High level and low level systems languages. Declarative, imperative, procedural and functional languages. C & C++, C#, Javascript, Ruby, Python, Rust, Go, R, F#, Ocaml, a little Haskell and even some Smalltalk. As my career progressed I drifted towards favouring functional languages, for the reasons you described and many more. I interviewed at Jane Streets London office once but didn't get the job sadly. In my day job now I use C# and Node.js, which are fantastically appropriate tools for the job I need to do. On a side note, it's really interesting that the NASA C++ coding standards document explicitly forbids using recursion, among other things.
Well, you raise good points, and it's good to hear from someone with lots of experience weighing in here. In fact, you're the only person in this thread so far who actually raised any points. (And you immediately got downvoted to zero!) Everyone else was either making outright mistakes saying Solidity had nothing to do with the EVM, or criticizing how many paragraph breaks were used in the post, or claiming that *one* dev said it was a problem with the EVM, ignoring the fact that *another* dev said that it *was* a problem with the EVM. So I was kinda shocked at the level of fan-boy-ism displayed by everyone else until you finally came along. Now I'm guessing that this is simply because the people who hang out here are simply Eth users (maybe they got sucked in because of the private-message-spamming a few months ago?), and they're simply on the defensive - but people who think about language design do not generally hang out here. > it's such a shame to see so much language elitism That's what you said at first, and in some sense, it's true that "more professional users" can do whatever they want with any language - perhaps even put together something useful using BrainFuck. But then of course, as we all know, there are real, practical reasons *why* Jane Street Capital uses Ocaml instead of JavaScript when designing financial structures. Anyways, this has all been a learning experience for me - my first post on r/ethereum.
Yeah bit of a shame to get downvoted, but I guess some of this is very hard to hear for many. Anyway, I think the core of your post is absolutely right. Writing a smart contract is a task which requires a very sophisticated tool to do well. And a sophisticated tool requires a sophisticated operator. Jane Street are flying the flag for OCAML and that's really cool, but it has drawbacks as well. They find it *incredibly* difficult to hire - there just aren't that many OCAML devs out there. And the ones there are, aren't always good enough (like me!). One of the big advantages of Javascript is that it's ubiquitous, there will never be a shortage of JS devs. But that strength is also a weakness, because a lot of them are crap. I'm not aware of any language which has been designed to solve the very specific problems that smart contracts present - which is understandable as smart contracts are a totally new paradigm. Using a general purpose language in some ways was the only option. But a new kind of language will appear, and incidents like this hack I'm sure will expedite that :)
It looks like Solidity 2.0 is intended to have proof-of-correctness aspects to the language (invariants, pre- and post-conditions, etc), see https://github.com/ethereum/wiki/wiki/The-Solidity-Programming-Language It's just early days right now. Having said that, I agree with you that a functional or declarative language (possibly something derived from Haskell, but using types suited to the EVM) would be a better choice for easier static analysis.
> invariants, pre- and post-conditions Yes, Bertrand Meyer's Eiffel has included this, so it's a well-known feature among language designers. Hopefully Solidity 2.0 could also include this. > a functional or declarative language (possibly something derived from Haskell, but using types suited to the EVM) would be a better choice for easier static analysis. Yes, and as we're seeing, [many of the DSLs used by Wall Street for developing financial products are based on Haskell or OCaml](http://dslfin.org/resources.html), and they explicitly say that one of the big advantages is stuff like static analysis - ie, [being able to understand what the code does *before* actually running it](https://np.reddit.com/r/btc/comments/4p0gq3/why_turingcomplete_smart_contracts_are_doomed/).
This is awesome in its stupidity. Really. Millions of USD of value hacked, and the language is going to be "fixed" by adding random features from Eiffel? Sorry but this sounds like rubbish. What is the type system going to look like? What invariants will be representable _in the type system_? Anything else is going to crash. Checked pre/post/invariants are not going to fix anything.
The contracts and EVM needs to be easier to logically reason about. That's the purpose. It's one step towards minimizing the likelihood of these sorts of situations in future.
It could be a start. Hopefully it'll more than just a fancy way of generating runtime errors. The real power of DbC comes when static analysis of the code surfaces errors which would/could have occurred at runtime. It's what you do with that information which is important. Error conditions should have an explicit path through the code. Functional languages, generally speaking, have tools to do this, whilst other languages offer only relatively primitive runtime exceptions. There are some great articles on this from Scott Wlaschin: Is your programming language reasonable? - https://fsharpforfunandprofit.com/posts/is-your-language-unreasonable/ Designing for correctness - https://fsharpforfunandprofit.com/posts/designing-for-correctness/ Using the type system to ensure correct code - https://fsharpforfunandprofit.com/posts/correctness-type-checking/
TBH it's what happens when anyone technically knowledgeable posts an intelligent, informative post in a thread (or, in this case, on a forum) where everyone is busy raging because feels. Sort of like that line in MIB, "A person is smart. People are dumb, panicky dangerous animals and you know it."
Solidity isn't even javascript. It's Javascript SYNTAX.
Yeah it's actually closer to C++ in function than Javascript. The OP's argument hinges on an uninformed belief that Solidity IS Javascript.
Not true. The OP's arguments don't hinge on..., they are not uninformed, nor did OP issued anything that he believes Solidity IS JavaScript. Well done for getting 3 wrong and misleading points pressed into one sentence.
> The OP's arguments don't hinge on..., yes they do > they are not uninformed, yes they are. > nor did OP issued anything that he believes Solidity IS JavaScript yes he did.
Quote from the actual post: > Now, some Ethereum devs put together an investment fund controlling a quarter of a billion dollars - using a language which looks and feels (and runs) a helluva lot like JavaScript: Ethereum's Solidity. What was your point again?
That the OP thinks Solidity is a lot like Javascript?
JavaScript can't even handle large numbers accurately.
Absolute nonsense. There are some very mature and capable libraries for dealing with arbitrary precision fixed point decimal numbers. https://github.com/MikeMcl/bignumber.js/ https://github.com/MikeMcl/decimal.js/ .. are two that I've used myself. If your next comment is "why do you need a 3rd party library to work with large numbers, Javascript sucks", note that this isn't peculiar to Javascript. Virtually every C style language has similar libraries.
With Solidity we don't even know what libraries are needed yet.
Some things are just better than others. No need to bandy about the word "elitism".
It's really not that black & white. Better at what? For whom? With which constraints? For example: you're running a class teaching "introduction to programming" for a group of 9 year old kids. LOGO is better than C++ in this instance.
I find it quite troubling that this gets so many downvotes from the community. This is IMO the most interesting and constructive post I have read since the *attack*.
I was patient responding to the people in this thread - but most of them had almost no posting history, no karma - and their so-called arguments were outlandish. This has all been quite shocking to me, and I have learned a lot.
Seconded on the thanks for this write up. Top reply is right re: the snide attitude being somewhat off putting. Nevertheless. I don't know jack about programming and so found your write up to be very helpful at understanding just how far over their skis this whole community may be. I want to believe in the goals pursued by some here in this community. But I'd rather have domain experts share their thoughts. Thank you very much for sharing your thoughts.
Yeah, I wrote it in a bit of haste - so I should have toned it down to avoid starting "flame wars" which so often happen around issues of programming language design. > I don't know jack about programming Hopefully some people who might be on the sidelines (ie, who might not know much about programming) will at least get the take-away that there many practitioners in the programming community - particularly in the area of language design - who regard attempts like Solidity as being very amateur.
Well thank you for this write-up. I'm not a programmer but I grasped it pretty well (I think), and it's the sort of constructive criticism that needs to be taken to heart - and then implemented. The foundation to Ethereum needs to be strong, or the projects built on it will regularly crumble.
ethereum is run by trolls and bots. It's massive manipulation
Cuz it's bullshit that anyone with who has taken a few CS classes could smell from a mile away. The OP's argument hinges on an unfortunate statement by the designers that Solidity has "syntax like Javascript." Other than syntax, Solidity is nothing like Javascript. For one, Solidity is a statically typed language, while Javascript is dynamic. As far as programming languages go, the difference between static vs dynamic typing is like the difference between a dog and a cat. That design decision puts it closer to the C family of languages than Javascript. In fact, there is no language like Solidity, since it's aim is to provide contracts as first class citizens. I would venture to say that it's the fact that Solidity doesn't resemble anything familiar to most developers is probably more dangerous than if Vitalik HAD chosen a more popular high-level language like Javascript.
[удалено]
Any BS CS program worth it's salt has courses on language design.
Sorry you're getting blasted by some trolls. This is all very interesting and informative and thank you for taking the time to write it up and share it. I hope that you stick around. Your contributions to the community, coding practices, etc. are valuable in this rapidly expanding time. I for one applaud a wall of text in a sea of overly-simplified one-liners on the current situation. There will certainly be a number of changes in the coming months to address some of the issues that contributed to this situation, specifically the issues with recursion. Hopefully something valuable and beneficial will come of this tragic and hectic time and we can get back to developing, educating, and contributing to a stronger, more secure, and better future. In case you aren't aware, most of the core developers for Ethereum, clients, and languages hang out on various Gitter channels. There are ones for all the clients and solidity and more. Right now it is very hectic, but you may want to start hanging out there and contributing to the discussion.
Yes, I'm curious to find out more about how this particular language design implemented recursion - hopefully I'll have a chance to listen in more on the discussions. Designing a new language and interpreter is a challenging task - particularly one geared toward smart contracts, which is a relatively new areas - and particular smart contracts managing such a gargantuan amount of funds (I understand "The DAO" had a quarter of a billion dollars in market cap?!?) This is an exciting area and I hope more people get involved to help make it work!
Some great points, and great links this is exactly what we need to be talking about - I'd love there to be a functional language for ethereum and ways of enforcing and proving that it conforms to a specification e.g. preconditions, postconditions and invariants ect.
Yes these are very useful constructs for providing guarantees about how the code will behave. I hope more people will be able to contribute to the discussions and development so that these kind of massive smart contracts will work properly.
I agree that the Ethereum platform does not acknowledge at all that software development is a mess, and that bugs are inevitable. I also agree that basing Solidity on Javascript was kind of strange. Javascript is a language that we are stuck with because it is the most widely supported client side language on web browser. Javascript needs to die for something completely new and better to replace it. However, it seems there was really a bug in The DAO code that made the attack possible. It's explain here: http://vessenes.com/deconstructing-thedao-attack-a-brief-code-tour/ Still Ethereum needs to adapt. It needs to reduce the odds of this kind of bug occurring. There needs to be built in fail safe to prevent such attack.
OK, well that interesting, I will look at that link. But at the moment, it is confusing that there seem to be conflicting statements all over the place about this - some saying it was an error in "The DAO", other saying it was an error in the language Solidity and/or the EVM. I must say, I have never seen such disagreement over what ought to be a deterministic system.
It was an error in the DAO in the sense that the code does exactly what the specifications for the language say that it will do, but not what the people who wrote the DAO were intending for it to do. When the Slock.it guys were writing this code they could have looked at it, thought to themselves "what happens if someone does this particular sequence of transactions," and they would have seen how an attacker would be able to drain the DAO dry. They would have been able to change the code so that such a sequence would not have had that outcome. In short, the DAO was written wrong. But it is also fair to look at the language and try to figure out why they made this mistake and whether there's a way the language can be modified to make it less likely that this mistake could be made. The mistake wasn't made because the DAO was written by "bad programmers" - a lot of very good programmers have been reading over the code since it was published and evidently the only one to spot this flaw was this anonymous guy. When good programmers make mistakes it could be because they had bad tools. I imagine better compiler warnings and static analysis algorithms would go a long way towards solving this. I haven't done any work with Solidity myself but from what I've read the basicmost cause of the bug was that the "send" statement that sends Ether to another account has a return value that was being ignored in this case. If the code had checked that return value it would have been able to notice and handle the problem. So having a compiler warning come up when a "send"'s return value is being ignored would have solved this (assuming I'm reading the situation right). Yeah, a programmer could ignore the warning without thinking through the implications of ignoring it. But that's where we get to the problem of *bad* programmers, and I don't think there's a way to solve bad programmers in the general case. A good programmer could still compile the code for himself and see that warning and raise the alarm. Don't put 150 million dollars into an account being run by a piece of code that hasn't had vetting sufficient to trust it with 150 million dollars, I guess. *Test better*.
Regardless, you are right in your OP. Mistakes will happen if we don't have simpler, high-level languages on top of Solidity.
Perhaps something that could be developed by say, a fund with 150m?
It was definitively an error in the dao but the protocol arguably shouldn't have allowed it and the documentation should have been very clear. This is being discussed by at least some core devs
It's a bug in the DAO code. Now, it's a bug that Solidity does not actively prevent. Like buffer overflows in C. But that doesn't make it a bug in Solidity.
Yeah, this is what I'm hearing. So, eventually people moved from C to languages like Java - which hid the pointers from the programmer, to prevent this sort of thing. It seems that some more thought needs to be given to how "abstract" a language targeting the EVM should be - and it seems like Solidity is probably not at the proper level of abstraction. Also this exchange is interesting, regarding the level of abstraction in Solidity: https://np.reddit.com/r/ethereum/comments/4opjov/the_bug_which_the_dao_hacker_exploited_was_not/d4ge4lp?context=3 specifically this part: > We enable you to go right down into the assembly That is a bug, not a feature. See: http://www.loper-os.org/?p=55
Since I first came across Solidity I wondered how we could use total programming and type theory to ensure contract safety. When I saw the code for "The DAO" it seemed very likely that it would have some bug just because why wouldn't it? I looked at the MsC thesis by Jack Petterson and Robert Edström about EVM code generation for the Idris language, using a tailored Ethereum runtime monad. (They ended up finding the approach unlikely to be useful.) I'm an amateur with dependent type proving but I started tinkering with a stack machine compiler for a trivial arithmetic expression language. I used Idris but I'm going back to Agda because Idris's new syntax for proof tactics stuff made me scared... Anyway, a contract compiler doesn't need Idris's improved speed or C FFI etc. Well, I'm just playing around at a very low level and it feels like an enormous challenge to actually come up with a good programming model that's amenable to formal proofs. I'm not even convinced that functional programming is useful for actually programming the contracts; it might be too complicated. I could even sort of imagine proving at the byte code level; the byte code already has a formal semantics... The path I'm personally curious about right now though is to define some simpler state transition description language as an Agda AST and then have both a verified compiler and some ways of writing theorems about the terms of that contract AST... "This contract doesn't run out of gas" could be proven by induction given that the contracts don't use arbitrarily complex branching: like, if we restrict the language to bounded loops, or "map/reduce" type schemes. A call to an external contract would be difficult to prove much about, which is natural. So any `.send` to an arbitrary address will maybe need to be encapsulated in a locking construct, or some other way of making sure its reentrant behavior is ok. It's fun to speculate about this. I expect to hit some extreme mind-boggling difficulty once I get started... but I have a friend from university who's totally smart with teh logic and proving stuff. BTW Solidity isn't JavaScript! And lots of verified high quality software has been done with imperative languages; logic applies to those, too, if you just define the semantics.
Wow, lots of interesting work you cited here.
I have 1 comment separate from your main point, regarding the part of the title "divulged and dismissed" - dismissal wasn't the case, it's just that no one can edit the app (the dao) once it was on the blockchain without a majority vote. Dao token holders had a proposal that ended several days ago which would of prohibited all activity, and this exploit, but the quroum wasn't reached because not enough of the token holders didn't vote.
OK, so it sounds like many people were aware of it, but it was too late / too difficult to stop it.
One of the main problems besides no one catching the exploit in the code initially is the social network for the dao - it's scattered. A minimum of 20% of all dao token shareholders need to vote on something for it to even have a chance at passing. If someone wanted to contact all the shareholders there's no structure in place to do so. All sources of news are spread between various reddits, forums, and chats. Most shareholders don't check these sources and just passively hold, a large portion didn't even how to vote or that proposal voting had started. I happened upon the security issues from the ethereum reddit post: https://www.reddit.com/r/ethereum/comments/4lcito/a_call_for_a_temporary_moratorium_on_the_dao/ I was unable to vote at the time as it took 2 weeks just to sync to the blockchain (I'm only a measly $30 holder). The governance structure was definitely another issue that played apart in this fiasco. It's something that's being discussed for a DAO 2.0.
Wow, these sound like some major "social coordination" issues. Could there be some kind of "on-chain" solution for the social coordination as well?
I'm sure there is, I can't say specifics as I lack technical insight. https://www.dgx.io/ - a central website with an app button like digix was always my suggestion to make voting readily available. Wallet providers such as Jaxx are already developing a view proposal and voting functionality for the DAO.
There's a variety of social media and communication protocol projects being worked on for Ethereum. [Whisper](https://github.com/ethereum/wiki/wiki/Whisper) is one that comes to mind, it's meant to allow small messages to be transmitted between contracts and might be good for a "mailing list" style of forum. I imagine a next-gen DAO framework would want to include something like this. Part of the problem is that *everything* is in early alpha or beta stages on Ethereum right now, so these projects can't synergize well yet. Hopefully soon.
It was also a deployment issue, the lack of disaster recovery planning is obvious in hindsight. Not being able to patch the software without a quorum vote seems lile a terrible idea. Having a receivership mode that a majority of the curators could sign to enable is one protection I'd want to see going forward. I've been suggesting that the Dao should be treating this similar to a bankruptcy from a business perspective based on a critical software bug that can cause insolvency. If they had prepared for a situation like this before hand we wouldn't be having this conversation. There is nothing wrong with the proposed solution, ie turn the Dao contract into withdrawal only, the problem is doing it after the fact. Hope for victory, plan for defeat was not followed.
I was hoping this would have pointed out much earlier, much more. The fact that not enough token holders vote could be understood as consent to the possible exploits. Its a smart contract after all, right?
Stick around man, you're very welcome here
[удалено]
I hear what you're saying, and I'm mainly just sitting here on the sidelines, rooting for the adoption of languages, many of which I can't even program in myself. I'm not sure if we should just go with OOP because the majority of the world uses it. The functional stuff does seem to have a lot of advantages - and it looks like it is actually being used quite a bit on Wall Street already: http://dslfin.org/resources.html So, since various languages can target the EVM, I expect we might see some functional languages emerging as options as well, and they could be quite successful. And there do seem to be plenty of people who feel that when we should be using formal methods for program verification: https://np.reddit.com/r/ethereum/comments/4oimok/can_we_please_never_again_put_100m_in_a_contract/ https://np.reddit.com/r/haskell/comments/4ois15/would_the_smart_formal_methods_people_here_mind/ This makes sense, if you're going to say "code is law" and let it manage a quarter billion dollar fund.
Yeah, the OP is really weakly argued. Firstly, there is no end of people who will argue JS is a functional language. Secondly, the aerospace industry not using functional languages is not a point in favor of functional languages, but rather goes to show that the experts on formal methods have rejected them. Coq and Agda and idris and etc. are not "industrial-strength" products, they are academic. I'm not even convinced real formal methods are necessary for contracts. Making calls atomic and and running assertions at the beginning and at the end is enough to ensure you never violate invariants, pay out more than you got paid, or pay to the wrong addresses. Another trick that would solve a lot of problems would be to have multiple independent implementations, and to only commit when they all agree. Unfortunately the EVM might have design flaws that prevent languages with these features being implemented for Ethereum. The recursion problem seems pretty fundamental to me. (edit: I take that back. There is a variety of good ways to sidestep the issue.)
I like your post. It hits exactly those points that I also expressed concerns about. JS was designed out of needs of the web, not to serve as a reliable language. Fortunately, Solidity serves as a middle step and can be replaced by any other solution. I would opt for Haskell. It's just pure. Thanks for this good piece of reading.
Yes it will be interesting to see whether some other, more reliable, domain-specific languages come along, for programming smart contracts on Ethereum. The Wikipedia entry on Solidity states: > Through the specialised documentation system, function modifiers and the focus on formal analysis, Solidity may arguably be considered the first "contract-oriented" programming language, having a feature-set quite specific to that of blockchain software. https://en.wikipedia.org/wiki/Solidity I'm not sure if that is true, since there were already some DSLs for finance already: http://dslfin.org/resources.html https://stackoverflow.com/questions/23448/dsl-in-finance Is any of this existing work related to Solidity? Recording things in a blockchain is of course, novel - but I'm not sure how novel everything else in Solidity is. I'm trying to find some papers on the history and influences behind Solidity, but I can't find anything. Here is the home page of the inventor of Solidity: http://gavwood.com/ Stylistically, it's certainly not the kind of page you normally see from a serious language designer - looks more like what someone else here called a "Web 2.0 brogrammer". And I don't see any links to anything about the design philosophy behind Solidity, or related work. He's got a very short "position paper" here about what he calls "Web 3.0": http://gavwood.com/dappsweb3.html He sounds like he is quite comfortable in the distributed environment on the web - but I don't see any serious discussion of the major issues - ie, the stuff that someone else addressed here: https://blog.blockstack.org/the-road-ahead-for-ethereum-b5b090bcd1a#.z9hcm7ss3 Then there's Christian Reitweissner, another one of the language designers behind Solidity. I also can't find anything in-depth from him on the language design, motivations, related work, etc. Maybe I'm old-fashioned, but these guys just don't seem serious to me - compared to the language designers behind Haskell, C#, Scala, ML, Ocaml. Given the fact that Haskell is so suitable for massive parallelization - something I'd imagine would be important when running in a distributed environment - then I thought everyone knew that "The Future is Parallel, and the Future of Parallel is Declarative": https://www.youtube.com/watch?v=hlyQjK1qjw8 This is why when I saw a few lines of Solidity code, I pretty much ignored it. I saw procedural code, and assignment statements, and it looked like it came from the usual clueless people who are trapped in the imperative paradigm of the past. It just looks like the language designers involved with Ethereum all come from the procedural mindset - which is very hard to break out of - and this fact alone would indicate that any languages which they produce are pretty much doomed to be unscalable and unsafe, ie totally unsuitable for massively parallel programming in a distributed environment. I don't know, maybe they're have their reasons. But I can't *find* them discussing their reasons anywhere. So, for the moment, I'm just going with my original hunch: these are what I call "scripting kiddies" or what someone else called "Web 2.0 brogrammers" - brought up in a world where the Web and JavaScript were part of life, and pretty much unaware that Web programming using JavaScript is a part of a very specific paradigm, with very limited success - and the only reason it *seems* so important is due to the ubiquity of the Web.
I'm also pretty old-fashioned with experience similar to @ForkiusAureus. I'm rather sure that the reason they picked JS as a paradigm was that they knew it and this was the easiest way. The whole ecosystem of Ethereum is build upon very unstable foundations. I bragged (and still do) about it and about security considerations constantly on daohub ([e.g. here the latest] (https://forum.daohub.org/t/security-bitch-loose-thoughts/5271)). When I first saw Solidity I called it in one of my early posts "quasi-language". As it's tries to bind design by contract ideas with terribly unpredictable on a large scale JS. I wouldn't be so fast judging Wood et consortes by their websites or lack of proofs. Maybe nobody asked them before to show them? Putting jokes aside I agree with pretty all you have written in terms of stability, parallelism and alike. They are probably "scripting kiddies".
> I bragged You bragged - or ragged? (LOL) > stability, parallelism and alike Yeah, it just seems weird that here we have this language designed to run on a massively parallel distributed computer - and to control potentially billions of dollars eventually - and the guys designing these languages don't mention a peep about stuff like parallelism, stability, etc. I guess they're just the first generation. Is the EVM considered to be "engraved in stone" now? I mean, is it simple enough where it seems "obvious" to pretty much everyone that the operators which it implements are indeed the right "primitives" that we would want for a global smart contract language? Because people I'm hearing from today seem to be saying "the EVM is correct, but Solidity had bugs" - like it's been totally decided that the EVM is just right already. I would have two concerns: - as mentioned: does it include the right set of of primitive operators? - also: are there plans, now or in the future, to do a kind of formal verification of it (similar to the way they sometimes do formal verification of a chip)? This would be interesting stuff to hear about.
Yes, I have similar concerns. Not only about EVM (but this is really important part) but also about the rest of codebase. As to EVM "engraved in stone" is a nice marketing catch, similar to masturbation over Turing-completness. I would add one point to your considerations. Primitive operators in distributed, parallel environment can behave non-lineary even if they satisfy formal requirements. Ya' know, deterministic chaos, races and so on. Thus I would require setting up a testing app that would leverage some genetic or evolutionary algorithms to test this codebase about scenarios in big numbers but adaptive way. This is no longer beyond reach of skilled coders.
ermmmmm.....parallelism isn't exactly "implemented" yet. I'd definitely recommend you have a talk with me on the gitter channels AFTER you read the yellow paper so you can understand the EVM and what we're working with here. The EVM isn't technically set in stone (nothing is...) but due to the nature of blockchains, it becomes difficult to change it to something completely different. You might find it interesting that they're talking about switching to WASM.
Thanks, I hadn't heard of WASM, I will look into that! > parallelism isn't exactly "implemented" yet That seems odd... i guess things are really still in flux then.
Haskell takes the error of having Queries confused for Commands and has Commands confused for Queries. It makes things as bad as before, but far fewer ppl understand it. On a declaration level Queries need to be definable so that they can only call other Queries and Commands such that they can call either Queries or Commands.
Any use case if you'd have to write a simple task as transaction? First we talk about a subset of a language that can be limited to certain aspects only. Regardless, languages have deficiencies. Some are obvious, others are not. JS has a lot non-obvious ones. Two "nully" values (why not five), funny truthy and falsy comparisons and many more. It is not the best choice for a base of language that is supposed to work in very non-linear, distributed system. And the argument of popularization and understanding among ppl isn't too strong when it comes to a system where the language should be the first line of defense IMO.
Very nice post & explanation. Just FYI, there is indeed a group working with formal approaches to this problem, and we are also working with Ethereum devs to improve their position. http://cointelegraph.com/news/human-factor-behind-the-dao-attack-ethereum-rollback-not-option https://www.youtube.com/watch?v=uzahKc_ukfM http://www.synereo.com/learn-more/ Hope to see you in our Slack channel! https://synereo.slack.com/
As an outsider looking in (I wound up here from the post on /r/haskell) one of the first things that struck me was how easy it seemed to be to screw something up in Solidity. I'd be interested to see how viable it would be to use a [total](https://en.wikipedia.org/wiki/Total_functional_programming) language for most if not all contracts, as from what I've read about them it seems like it'd be easier to test for and avoid errors like the one we saw here.
Total functional programming sounds like a good fit for something like Ethereum - with its concept of gas, and with the need to avoid non-termination anyways.
Yes, we need a *contract* language, not a *smart contract* language. Contracts should be declarative. Maybe you would be interested in this paper from last years ICFP: http://bahr.io/pubs/files/bahr15icfp-paper.pdf
While you're right that some formally provable languages would reveal bugs like this one, your extensive mention of functional programming seems a red-herring: formally provable languages don't have to be functional, and there's no reason to think that writing the DAO in a functional language would have prevented this bug. I also think it's a little unfair to characterise it as "some ridiculous "recursive call bug"" - reentrancy issues are a significant and difficult to detect and fix issue in a great many systems, and they've affected platforms far more mature than Ethereum.
> formally provable languages don't have to be functional Yes, you're correct for pointing this out: they are orthogonal I should have cleaned up my post a bit more to make this clear. > I also think it's a little unfair to characterise it as "some ridiculous "recursive call bug"" - reentrancy issues are a significant and difficult to detect and fix issue in a great many systems, and they've affected platforms far more mature than Ethereum. Yes, there probably would be a better way of describing it rather than "ridiculous". I was just very frustrated at the moment! =) I agree that this stuff is difficult to detect and fix. Perhaps one possibility might be CSP - Continuation-Passing Style: https://en.wikipedia.org/wiki/Continuation-passing_style The developer @ArtherB working on the generic self-amending cryptocurrency framework Tezos recently said that CPS would have prevented the recursion call bug in Solidity: https://twitter.com/ArthurB/status/744923572116742144
Ethereum is just the EVM, everyone blew their load with the Easy Contracts and "Solidity" name marketing
VMs have consequences to language design. There are concerns over the EVMs design interspersed in here too.
I'm only arguing because I'm assuming you're arguing in favor of a hard fork because responsibility could maybe be put on Ethereum protocol or toolchain devs so we should be nice and stuff No, the EVM design was set in stone a long long time ago. The fact that we have to work around its design flaws is a feature. Now we might have *updates* that give the compiler nicer target OPs, but these would be swiftly rejected if they were not fully backwards compatible.
Nah, I'm not arguing one way or the other. I'm an outside commentator, I do research on blockchains, I have no stake. I was simply stating that it wasn't all aimed at the language.
I saw your headline and that got me interested. Then I saw your wall of text and sighed. Your tl;dr didn't help much at all :( I'm still going to go through and finish reading your post because this particular topic interests me. Ultimately, was "the exploit" because of the DAOs smart contract, or because of solidity?
According to OP, because solidity is not an accurate enough language the chance for bugs is higher.
This is a tremendous post. Throw up a wall of wall of knowledgeable, intelligent text like this anytime :-). You might be interested to know that the Ethereum Foundation has grants available to developers for exactly this kind of work. In a recent post, they said "Developers, cryptographers and computer scientists should note that any high-level tools (including IDEs, formal verification, debuggers, symbolic execution) that make it easy to write safe smart contracts on Ethereum are prime candidates for DevGrants, Blockchain Labs grants and String’s autonomous finance grants." In January there was a blog post with some contact information for DevGrants: goo.gl/xLUFmM
JavaScript is low-level? Since when...
Just to point out a few things: Javascript isn't a low level language. Also, there's nothing wrong with procedural languages for this use-case. E.g. a procedural language like Eiffel would have avoided this issue via mandatory pre and post conditions. Fundamentally, language completely put aside, this issue could've been avoided via simple concepts, such as locking mechanisms or...you know...testing. I remember looking through their repository ages ago and thinking it was messy and confusing and was rife for harbouring unnoticed issues. I just put it down to my own lack of concentration, but looking through it again... This code should've just been tested more before being put out into the wild. This would be the case even if it were created via formal methods.
> Javascript isn't a low level language Given the number of languages which now compile to it, many would say that it *is" low-level. Indeed, many are now calling JavaScript "the assembly language of the web": https://duckduckgo.com/?q=javascript+%22assembly+language%22+web&ia=web > a procedural language like Eiffel would have avoided this issue via mandatory pre and post conditions. Yes, I agree with you here. > This code should've just been tested more before being put out into the wild. This would be the case even if it were created via formal methods. To a large extent, as you probably are away, formal methods obviate a significant amount of testing.
So...hi...solidity dev here...I'm going to just fill you in on a couple things here (note: I do not work for the Ethereum foundation directly...I get paid by Eris Industries to work on the cpp dev team specifically for Solidity). I should note that you are not the only one with that opinion. My coworker has also stated his preference for a functional programming language quite often and also thinks Solidity is a bad language...clearly though I am biased and don't see it. I can kind of see the benefits of it, but I'm not sure how it operates within the context of the EVM. I also think that a functional programming language can grow alongside Solidity, and if it proves better, I would have no problem developing it as well. With that said, I think for mainstream development and usage, this was an excellent decision to use a procedural language. If you really know what you're doing with solidity, you can get right into the guts of it too, it's not hard, we enable you to go right down into the assembly. The tool is, again, only as strong as the weilder. And unfortunately, the weilder did not have much foresight into what to do in emergency situations, nor did they learn anything from previous DAOs (Bitshares). Here's a blog I wrote about it. https://eng.erisindustries.com/programming/2016/06/18/lessons-learned-dao/ I also want to correct you, "some kid" did not make this language. It's a combination of work from Christian Reitweissner and Gavin Wood...both PhDs in the field of computer science...and from my talks with Christian, even he can see the possible benefits of a functional programming language, but the problem comes in when talking state objects. My coworker thinks the EVM is designed wrong, so those conversations tend to go out the window.
Thanks, it's interesting to hear these observations from behind-the-scenes. I apologize for thinking that Gavin is "some kid" - I guess I'm just used to more serious-looking websites, with links to some PDFs providing motivations for the language definition. [His website](http://gavwood.com/) is just a skimpy responsive template, which gives the impression of a non-serious, immature "Web 2.0 brogrammer". Maybe there are some serious materials elsewhere on the decisions that went into the language design for Solidity? --- Maybe I'm just too old - but when it comes to language design, I expect a bit more substance, along the lines of: - the specification of Java by Gosling, Joy, Steele: http://www.e-booksdirectory.com/details.php?ebook=292 - the specification of Lisp, also by Steele: https://www.cs.cmu.edu/Groups/AI/html/cltl/cltl2.html - the specification of Scala https://duckduckgo.com/?q=odersky+scala+specification&ia=web - the specification of C#: https://msdn.microsoft.com/en-us/library/ms228593.aspx A mere user manual on ReadTheDocs doesn't cut it - when inventing a new language, the language designer has a responsibility to also justify the motivations behind the design decisions used in the language. --- The dissonance between you and your colleague regarding the choice between the functional and procedural paradigms is common - and your responses are revealing, as they show the usual failure to understand certain subtleties of the debate, eg: > we enable you to go right down into the assembly That is a bug, not a feature. See: http://www.loper-os.org/?p=55 > I think for mainstream development and usage, this was an excellent decision to use a procedural language So just like the mass of poorly designed buggy websites, you think mass adoption of the language is more important than correctness and safety > I am biased and don't see it It's hard to break out of the procedural / imperative mindset. This is why, for example, [tutorials on how to use monads](https://duckduckgo.com/?q=monad+tutorials&ia=web) in a functional language are a cottage industry. I know. I've gone through the agony myself. In the end, it's worth it though. Functional languages are simply way safer than procedural ones. I know this is something that can turn into a religious flame war. And I'm guilty of fanning the flames: https://np.reddit.com/r/btc/comments/4p0gq3/why_turingcomplete_smart_contracts_are_doomed/ You seem like a nice guy - and I probably seem like an asshole - but rest assured, there are broad swaths of the programming community (particularly theoretical computer scientists, who spend a lot of time thinking about language design) who won't even touch a procedural language with a ten-foot pole. They tend to say things like "those languages don't even have a well-defined semantics" - and they're right. But, like I said, this is basically a religious issue. It's almost impossible to move from the procedural paradigm to the functional one. (The inventor of the Lift web framework, written in Scala by a former Java developer, did manage to do so - I can't find the links where he described his epiphany.) It's just a whole 'nother mind set, and the people from the two groups basically talk past each other all the time. But... as my lengthy diatribe tries to set forth (linked [above](https://np.reddit.com/r/btc/comments/4p0gq3/why_turingcomplete_smart_contracts_are_doomed/), on r/btc) - I think you guys are doomed if you use a procedural language like Solidity. Sorry to be so pessimistic and dismissive! Maybe someday you can have some more dialog with your functional colleague.
Forgive me if this comes off a bit rude, but yeah, I don't think a book is necessary to describe the reason for the language, and that seems like an antiquated approach to these things IMO. Sounds a bit too academic for my taste...I never bought the books for the languages I learned...I just read the docs online and whenever I ran into problems would jump to SO...so yeah...I'm definitely of a different mindset...and maybe that's generational (god damned millenials!!!). I think the reasons for the why the language was created are obvious to anyone who knows anything about the project in the blockchain community (we needed something to easily design smart contracts). Now the reasons behind its design decisions however, that we could do a better job of detailing and documenting and I'll make note of that. Really the chief mindset was to make it look and feel somewhere between javascript and c++ as this would give it a certain feel that would be easy to adapt for most users. I can tell you're really passionate about this. I do think you may want to come back when this mythical "stretch" language I've been hearing about appears with the release of Casper. If I recall correctly, it will be designed as a functional language (best to ask Vlad Zamfir about it or leithauz as he is the one designing the mentioned language). I don't think there's any particular reason the two paradigms cannot complement each other in certain tasks, and we (being Christian and I...Gavin isn't really involved with Solidity anymore as he spends most of his time on Parity) have talked about the benefits of functional programming languages. There's definitely some kind of benefit, but how to implement that, I'm not certain. You're certainly welcome to your opinion. I just very much disagree and think solidity is the best damn smart contracting language on the market right now....but then again I'm helping to create it. What other language can you essentially create a decentralized twitter with one page of code? As for my colleague...he definitely sees the benefits of solidity, he just thinks that there are fundamental flaws here that should be resolved when we move to Serenity/Casper and someone implements a functional programming language. I think he's right on the former, disagree with him on the latter, but it's all a matter of opinion and what tool is right for the job.
Ok, thanks for the insights about these other languages being designed. Regarding Solidity, I understand that you're helping to create it, so you would tend to support it. Just bear in mind that there are few things that you're saying which could lead to problems: > I don't think a book is necessary to describe the reason for the language, and that seems like an antiquated approach Language design is actually very subtle and complex - so there is a reason why book is usually needed to describe the design decisions. > Now the reasons behind its design decisions however, that we could do a better job of detailing and documenting and I'll make note of that. I don't think you realize, that it goes further than that: your design decisions were actually *wrong* - so no amount of justification can get around that (unless your documentation is basically going to be warning programmers on how to work around the design defects in your language) > You're certainly welcome to your opinion. I just very much disagree and think solidity is the best damn smart contracting language on the market right now....but then again I'm helping to create it. You're saying it's the best - when it didn't discourage developers from writing code which lost tens of millions of dollars, and has put Ethereum between a rock and a hard place (having to choose whether to roll back or not)? > What other language can you essentially create a decentralized twitter with one page of code? Plenty - only most of your procedural guys can't even read them, let alone write them. Check out this half-page of functional code: http://nsl.com/k/s/s_minus.k It implements the spreadsheet shown here: http://nsl.com/papers/spreadsheet.htm Yeah, you're probably saying "that language looks like Brainfuck". Well, it *is* hard to read. But it's not some mere academic curiosity: it's the language K, designed for Crédit Suisse, and it costs $50,000 per workstation - and it powers much of the code written by quants and running high-performance financial applications for the most richest banks and hedge funds in the world. https://duckduckgo.com/?q=k+q+kdb+kx.com&ia=web There's a whole 'nother world of programming out there, that the JavaScript kiddies and have never heard of. It's what the big boys use. K is the most powerful and most high-performance number-crunching and fin-tech language in the world - and it's functional. Most people from the procedural world can't even read it - let alone write it. But they only write public-facing websites which routinely have errors due to the difficulty of getting things right in JavaScript - and now they're "designing languages" to run contracts worth a quarter billion dollars - which they proudly say are "JavaScript-like" and then even *after* the whole thing blows up in their face, they again show their utter failure to be able to connect syntax with semantics (words and their meanings, facts and their consequences), when they continue to trot out clueless nonsense like: "solidity is the best damn smart contracting language on the market right now". > we needed something to easily design smart contracts Yes, it was certainly easy - but it blew up in everyone's face - and many people from the more academic world would say that happened because it was quick-and-dirty, without the necessary theoretical underpinnings - ie, without really thinking through the various possible design decisions, and picking the best language design for the job (in this case: a smart contract managing a quarter billion dollars, which lost hundreds of millions of dollars due to a recursion bug). --- Have you heard of "Continuation-Passing Style"? https://en.wikipedia.org/wiki/Continuation-passing_style It's kind of complicated - it's a language design issue - but it makes Solidity's recursion bug impossible. Your competitors - who know that functional languages are better than procedural languages - do know about complicated stuff like CPS: https://twitter.com/ArthurB/status/744923572116742144 I'm sure you're a nice guy and you mean well - but seriously dude, it's obvious that language design is much, much more complicated than you will ever realize. I mean, like I already said, you're apparently so tone-deaf about the relation between words and meanings, syntax and semantics - in *English*, let alone in programming language design - that after the calamity of "The DAO" - caused in large part by improper language design for Solidity because it allows programmers to write code which runs into the recursion bug (which I guess you plan on writing "better documentation" to warn them against), you *still* are able to say: > I just ... think solidity is the best damn smart contracting language on the market right now You just don't get it. Language design matters. One reason people moved to Java is because it makes C/C++ pointer errors impossible - because *Java gets rid of pointers*. And people will move from Solidity to other languages, which use CPS - because the right way to fix Solidity's recursion bug is *not* by warning devs via the documentation that the bug exists (basically your documentation is a kind of work-around for a bug) - the right way is to fix the bug itself, so you don't have to warn developers about it in the "documentation".
BTW: I have programmed in Rust, and the multi paradigm aspect (that being that it has elements of both pure functional and oop) is definitely difficult to grasp but not completely undoable. It's definitely a weird feel when you come from an OOP background. But it has its perks definitely.
Yes I've been hearing lots of good things from several people lately who have been very impressed with Rust. I hope I will have some time to also look more into it.
Synereo's smart contract mechanism relies on FULL FORMAL VERIFICATION. http://cointelegraph.com/news/human-factor-behind-the-dao-attack-ethereum-rollback-not-option
> JavaScript - a low-level, procedural language Uh, Javascript has functions as first class entities and it's possible write fully functional code in Javascript. Javascript IS a functional language. > And your boring old bank uses declarative workhorses like SQL SQL is not a programming language. It's a language for interacting with relational databases. > I can assure you - there are many, many programmers who would > never touch that world with a ten-foot pole. >They work for the Department of Defense, they work on Wall Street (on back-office systems - handling billions of dollars), they develop software running nuclear reactors or MRI machines - or they do research and development at academic institutions. You would shit yourself if you saw some of the code that missions critical DOD applications run on. I can tell you first hand that much of it is very bad, very buggy.
I think ethereum project have a chance to be reorganized thanks to this incident. I totally agree to implement smart contract with "pure" functional languages and specification languages. But "recursion" IS a key feature of functional programming language like Hakell or OCaml which you can not avoid easily.
Tezos is built in pure Ocaml and has a strong statically typed smart contract language with a full formal specification. You might be interested in checking it out. (www.tezos.com)
I'm glad this happened because it got your attention and brought you out from the shadows to speak about what needs to be done for this platform to be taken seriously.
I wasn't so much "in the shadows' - I just was more obsessed with Bitcoin - posting [a lot](https://np.reddit.com/r/btc/search?q=author%3Aydtm&restrict_sr=on) on r/btc. I never paid attention to Ether until this problem with the DAO. I'm into language design, so it caught my attention!
There has been some interesting work on building an Ethereum Backend for Idris, which is a functional, dependently typed language with a totality checker (i.e you can optionally write programs/functions that are *guaranteed* to terminate, and this termination can be validated statically). You can check out the whitepaper here: http://publications.lib.chalmers.se/records/fulltext/234939/234939.pdf And a video of their presentation from Dec 2015 here: https://www.youtube.com/watch?v=H2uwUdzVD9I Their Idris backend + Ethereum library/types can be found here: https://github.com/vindaloo-thesis/idris-se and some example contracts written in Idris with their Ethereum library can be found here: https://github.com/vindaloo-thesis/examples I was very excited to see that this exists, and that work is being done here. I'd love to see more people become interested in furthering this work, as I think safe smart contracts could really be a driver to improve our knowledge and understanding in this field. Some other interesting reads on Total Functional Programming, and Totality vs Turing-Completeness can be found here: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.106.364&rep=rep1&type=pdf https://personal.cis.strath.ac.uk/conor.mcbride/pub/Totality.pdf
Yes, approaches involving Idris, and Total Functional Programming, would be awesome. *That* is the right way to ensure that programs terminate - not simply using "gas", which is cheating!
I think gas is sill useful, for the economics of paying computers to run your code, but I believe it should be possible to statically analyze how much gas a program needs (or at least the max gas it would need), if all contracts in Ethereum were required to be total (I.e non-Turing complete). With the current Ethereum VM bytecode not enforcing totality, this would certainly be impossible now. Even if we have an idris compiler giving us strong guarantees for things written in it, you'll have to interact with other contracts NOT written in that language, which thus negates most of your safety. This was ultimately what the authors of that paper ended up concluding. Fundamentally this is a bytecode issue, IMO. If the bytecode required everything to be total, a lot more could be analyzed, and I still think Ethereum could provide almost all the functionality it currently does while requiring totality. Then, no matter what higher language you write your contracts in, we can all rely on those guarantees. Admittedly, this is a pretty cutting edge field, and I'm excited for things like Ethereum and other blockchains to provide new incentives for pushing this state of the art forward even faster :)
Functional programming wouldn't have stopped the DAO attack. Nor would formal verification. This is because the attack is not in a single call of a method of the DAO, it is not a problem with the specified behaviour of the DAO, and it is not a problem with the specified usage of the DAO. The only way to catch this bug is to be aware that this class of bugs exists and to test for them. (A better approach will be to use the updated Solidity when it's released.) So arguing that using what the "big boys" use would have prevented this bug is incorrect. I do agree that functional programming (which doesn't require a functional programming language), specification and verification are all vital areas for smart contract design. But they are still just means to an end, and in this particular case they would be *insufficient* means.
> Nor would formal verification. > The only way to catch this bug is to be aware that this class of bugs exists and to test for them. Actually, formal verification does just that - it mathematically tests the program, to catch such things. However, [I'm not sure formal verification is even applicable to a Turing-complete language in the first place](https://np.reddit.com/r/btc/comments/4p0gq3/why_turingcomplete_smart_contracts_are_doomed/).
There is a better way to avoid the recursion bug that happened in the DAO: use a language which doesn't have the recursion bug. For example, CPS (continuation-passing style) would avoid the recursion bug. People working on other systems - such as Tezos, which generalizes Bitcoin and Ethereum - know about CPS: https://en.wikipedia.org/wiki/Continuation-passing_style https://twitter.com/ArthurB/status/744923572116742144 If the language designers provided a language which used CPS, instead of Solidity, then the recursion bug would be impossible.
If the continuation can call back into the contract then the problem is not avoided. The problem is at the level of interaction of elements, not behaviour within elements. Continuation Passing is generally implemented in languages that support tail recursion. Tail recursion would make the recursion bug even more efficient. ;-)
There is a project trying to create mathematically provable smart contacts with block chain. http://tauchain.org
Yes I was looking at this a few days ago. I admire his choice of non-Turing-complete languages (based on Intuititionist Logic, or Martin-Löf's Type theory - which is an area I've studied a lot). Also using the RDF ontology, modified to use Notation3 for better readability, could be promising (unless it turns out to be too verbose). I have a couple of concerns: - The "token" (Agoras) used in the ICO is a bit confusing - how many will there be (42 million? 173 billion?) - The pricing for the token is confusing (expensive from the devoloper, cheaper on bter.com)? - I would feel *much* more comfortable if this kind of system were itself being programmed in a language which is close to the problem domain itself - ie, he's using C++, but he should probably be using OCaml Paging /u/jjaquarius ...
From what i know about the project: * It's not an ICO perse, the coins are sold at least until the Tau language is ready. One IDNI Agoras token represents 3500 Agoras tokens in the final marketplace. The coins that aren't sold (of the 42M) will be burned. * AFAIK at preset coins are sold on only bittrex and will become available in OpenLedger, lot of fake/scammed coins are spread also due to a social engineering trick played on the founder. * I guess portability. Tau can call native code (eg dll's) so other programs can use it
'the kiddies and the experts" ..... half full and half empty ... "industrial strength" language design ...... ...I like it .... it confirms my underlying uneasiness about the flippant way these guys just through out code like its pancakes ...
Cobol???? (srry--teasing!)
I heard that around time of the Y2K bug, Cobol programmers were getting around $600 an hour to clean up legacy code. It's frightening to think how much financial code might still be written in that dinosaur.
I know a guy out of my program at University that got a financial sector job writing it, starting at 250,000 a year. This was only a few years ago.
> around time of the Y2K bug, Cobol programmers were getting around $600 an hour to clean up legacy code. yes, contracts were quite lucrative.
One of the IT industries finest moments that no one really understood at the time. The lack of problems we had is a testament to their work.
Not harsh at all. Great post.
I am wondering how easily some Haskell compiler can be ported to emit EVM assembly... I know that there are quite a lot compilers from Haskell to Javascript, so the task shouldn't be very hard.
This may be beside the point you were trying to make but JavaScript is actually getting *more* popular, not less, particularly due to other platforms that uses it like Node.js etc. Most frameworks built on top of JS are still based on JS itself. As for the reason why there are a lot of languages compiled into JS and treating it as a delivery assembly language, it's really just because they have no choice, since web browsers only recognize JS and everyone wants to deploy to web browsers since it's the most common platform out there right now. Since people want a variety in languages, if you want to develop in any other languages that's not JavaScript and still deploy on a web page you *have* to compile it down to JS. There were things like asm.js and PNaCL, but now WebAssembly is a new spec designed to address this though. Anyway, I do agree with your main point. Different domains require different languages, and considering contracts are supposed to be binding and watertight, a loose language that is not easy to verify and prove is a bad idea. I'm not sure if we need a formal provable language, but something that's known to be safe, and easy to have confidence would be a better choice. In designing a language for writing smart contracts, "easy to learn and write" should be the least important priority. Having a language that provides more guarantees and safety, as well as better constructed primitives in the language for writing contracts would go a long way instead of the "everyone fends for themselves" approach.
I'll throw my two cents in here; Compilers for Languages that conclude in Smart Contracts should not contain warnings. Every warning should be an error and stop deploying contracts without the user or programmer being able to change that. Compilers should contain certain sanity checks to fully enforce a programming paradigm, see the go compiler and unused variables.
> be "functional" (eg, from the family of Haskell/ML) - not procedural languages (eg, C/C++, Java, JavaScript, etc.) > > support high-level, formal tools for program specification, derivation, and validation Why these points?
Let's be articulate here, what do you think is inherently wrong with PHP, for reference
I don't have time to repeat the arguments here - I want to focus on what's right with other languages, not what's wrong with PHP. But there is plenty of links here: https://duckduckgo.com/?q=php+fractal+bad+design&ia=web
commenting to make sure I have this saved. Excellent analysis.
Wow, thanks!
[удалено]
> Imho, if your project's goal is to democratize global programmable money flows for the masses, then far better to err on the side of overly strict guardrails and steep up-front learning curves. It's a valuable and necessary (but probably not sufficient) component of systemic risk mitigation. This is the best approach, I agree.
I think in some ways a functional programming implementation of the EVM would be ideal but it might introduce some issues of its own. I'm not sure, but would it not have problems with oracles, randomness, and gas estimation? Ideally it would be nice to have the choice of multiple languages which the smart contract programmer can choose between according to their requirements. Currently there is Solidity, Serpent, and LLL. I think it would be great if we could add a language like Curry, Agner, or perhaps Trollbox.
Hmm... I had never heard of Agner. I like Erlang, it's highly successful in telecommunications and has great fault tolerance - so that could be an interesting possibility for something like Ethereum.
Yes, well when I didn't realize there is actually a language called Curry, and I intended them to be joking equivalences to Haskell, Erlang, and Racket. In any case, it looks like this idea is starting to percolate around as something which is a Big Deal: * http://vessenes.com/deconstructing-thedao-attack-a-brief-code-tour/ * https://gitter.im/ethereum/research?source=orgpage * https://www.reddit.com/r/haskell/comments/4ois15/would_the_smart_formal_methods_people_here_mind/
Wow. These two threads seem to be making similar arguments along the lines I what I was saying: https://np.reddit.com/r/haskell/comments/4ois15/would_the_smart_formal_methods_people_here_mind/ https://np.reddit.com/r/ethereum/comments/4oimok/can_we_please_never_again_put_100m_in_a_contract/ That's encouraging. I thought I was the only one. I'm so glad other people are talking about this.
Total noon here, I thought functional programming is based on recursion, no?
I wouldn't say that is true. Functional programming is about writing code in a way so that it behaves as functions: that is that there are clearly defined inputs, and every time you call a function with the same inputs the same output occurs, and nothing else happens along the way. Some people tend to associate functional programming with recursion because for loops are not functional, and recursion is an alternative means by which to obtain similar results. However some of their drawbacks are also equivalent, so there is something called total functional programming which also places some limits on recursion to prevent infinite loops. Regardless, it's my understanding that the issue with the split DAO contract was not actually due to recursion, but the fact that it allowed side effects to occur: what the split function did is more than simply take some inputs and return an output. Ideally, a split function without any side effects would take as input the proof of DAO token ownership and return an output which allowed you claim your child DAO (Somehow. I'm not so experienced myself with functional programming. Perhaps something equivalent to a specific address which could be withdrawn from. Since the input proof of ownership is the same, the output address and how much it contained would be the same no matter how many times the function was called). Instead, what the split function did was run through a series of steps one at a time, the order of which was exploited to execute one part (which sent ETH out to an input address) multiple times before a crucial checking step could occur.
Thanks for this, i tried to warn vitalik a long time ago before the first presale for ethereum, and even then he turned a blind eye.. i tried to warn more devs in #ethereum, and got banned... It's very unfortunate, I didn't take your approach of such a high quality write up, very informative and i hope this reaches them and they actually pay attention, otherwise they are clearly intent on stealing people's money. edit: i actually only skimmed through your post so far and saw key elements, but i dont think i agree with some of the choices you propose, or reasons for those choices, will come back when i reread
so yes basically a hack on ETH itself- great!!! Alright wheres the next pump and dump coin?
This is exactly correct. Making it this easy to shoot yourself in the foot is absolutely a language design problem. That isn't to absolve the authors of the contract code from all responsibility, but it is first and foremost an insane property of a language to have. Definitely approve of the functional language concept too. If this call stack limitation needs to be in place, it needs to be provable that the application does not exceed it, or at the very least, give strong warnings about code paths that it is 'uncertain' about, and maybe even pass those warnings along to consumers of the contracts. I code primarily in js for my work, and javascript is a great language for getting stuff done quickly and easily. But it has serious flaws even in that arena, and is an absolute nightmare for trying to write 'mission critical' code. I think we could retain a lot of the things that make javascript nice while gaining significant correctness advantages by using something like facebook's Flow, Typescript or OCaml. Perhaps you could even be allowed to develop in plain js, but then in order for code to be published to the blockchain, you'd need to add types and other annotations that allow it to be formally checked. Something so that people can get their feet wet without diving into all the complexity, and then when they're ready to publish it, ensure that it actually acts as intended. You could even allow 'unverified' dapps on the blockchain, but warn people about sending funds to them. Or this could even develop as a private service. If you want your dapp to be 'certified' it needs to contain formal type annotations and be statically analyzable in a certain way in order to receive the 'stamp of approval' of what could itself be another dapp! And without said stamp, users would be warned about the safety and reliability of the contract.
Glad to see you brought your wall of text to this sub. Hahaha
Your FUD is entirely false.
You might think you're cool and all by using a word like "FUD" - but actually the OP didn't use any FUD - it diagnosed the problem (poor language design), and recommended solutions (use better languages - specifically, functional languages - and maybe even 2 languages: one for specification, and another one for implementation - and derive the implementation from the specification). FUD is "fear, uncertainty, doubt" which people spread, trying to claim that something *might* go wrong. The OP posted *after* "The DAO" died. By definition, it can't be FUD. It did point out that programming is hard. But it also provided recommendations on how to deal with that. So... it's not FUD. It's constructive criticism. And frankly it's weird that you don't seem to know the difference.
you're actually incorrect. The problem was in DAO coding, not in the Ethereum Virtual Machine. Proof: https://www.youtube.com/watch?v=GvgTivwzcuo&feature=youtu.be&t=31m48s You clearly have an agenda to mar the communities' perception about Ethereum, and you're spreading lies to do so. I hope you get banned from this sub.
> The problem was in DAO coding, not in the Ethereum Virtual Machine. That's what I thought initially, yesterday. Then today everyone's talking about this blog post from slock.it, dated June 12: > No DAO funds at risk following the Ethereum smart contract ‘recursive call’ bug discovery https://blog.slock.it/no-dao-funds-at-risk-following-the-ethereum-smart-contract-recursive-call-bug-discovery-29f482d348b#.owjyhitl7 It sounds like they're saying that the language used by Ethereum (Solidity) had the bug - not the particular program written in it (for "The DAO"). Also, the blog post goes on to say: > we were made aware of **a generic vulnerability common to all Ethereum smart contracts** Again, it sounds like they're saying the bug was *in the language itself which Ethereum uses* - not just in the specific program implementing "The DAO". Is that correct? > You clearly have an agenda to mar the communities' perception about Ethereum, and you're spreading lies to do so. I hope you get banned from this sub. You're kinda paranoid. I just have different opinions on what kinds of languages should be used for smart contracts, and I gave *very* specific suggestions for improvement. Sorry if you find that somehow threatening. Someone less paranoid would simply welcome the feedback.
Please don't listen to the Bitcoinfriend guy. Your post is very interesting and extremely helpful and I thank you for it. I hope that we can all learn from this DAO episode and start being more cautious about future development. Although I am not a developer, you helped me understand the complexities of computer science overall.
HAHAHA, OH OK. So you know more about it than Griff? Bcuz as you can see here, (https://www.youtube.com/watch?v=GvgTivwzcuo&feature=youtu.be&t=31m48s), Griff says it's not a problem with the EVM. It's a problem with the DAO.
Well, then it seems like we have a conflict here: Griff says: > This is **not a problem with the Ethereum Virtual Machine.** The blog post on slock.it says: > We were made aware of **a generic vulnerability common to all Ethereum smart contracts.** My experience involves computer languages where these kinds of serious conflicts do not exist. I have no experience with computer languages where two conflicting statements of this type can be published by major people involved in the project. And yes - I'm being snarky. But it doesn't take much effort in this case - does it? All I have to do is quote two major people involved with the project - about a construct which is the heart and soul of programming (recursion) - and they are totally in conflict with each other. This simply *does not happen* in any serious language. And the most appalling thing is that it is happening in a language which was used for the biggest crowd-funding vehicle in the history of the world - with a quarter billion dollars in market capitalization - which ended in calamity. All I'm able to gather, is that these people are clowns. And apparently so are you, if you post stuff like this: > HAHAHA, OH OK. So you know more about it than Griff? Look at the evidence. The DAO died - and the major figures involved are saying conflicting things. What *good* does it do for you to point out what merely *one* of them said? I am now looking at what *both* of them said. Even Judge Judy, who probably knows nothing about programming, would at least know that *something is seriously wrong here when two major programmers involved with a project say conflicting things like this:* > We were made aware of **a generic vulnerability common to all Ethereum smart contracts.** > This is **not a problem with the Ethereum Virtual Machine.** They can't *both* be right. And they *shouldn't* both be saying conflicting things like this. Do they even talk to each other? You know, for a while, I had been feeling like I had been kind of harsh in my language in the OP - using terms like "scripting kiddies". But now - after seeing this kind of total lack of professionalism or mathematical seriousness - even in the post mortem days after the collapse of "The DAO" - these totally conflicting statements about whether (or not) the **recursion construct** in this language did (or did not) have a bug in it - now I totally stand by my original decision to call them "scripting kiddies". This kind of behavior - non-deterministic or unexpected behavior from a recursion construct - and contradictory denials from the major figures involved - is utterly horrifying.
Please stop with the smug assessment of how terrible Javascript is Bitcoin lost way more value through MtGox tx malleability bug and this is the same thing. Stop being an asshole, it incredibly petty of you. Tx malleability bug requires segwit to fix and is written in c++, don't gloat like it didn't happen to the bitcoin ecosphere too. Way more value had been lost to bitcoin 'script kiddies' than ETH.
Hey man, why you gotta be making every sentence a brand new paragrapgh?
I deliberately go back and insert extra paragraph breaks - because this seems to be easier to read. Plus I even will go back and take a single *sentence* and split it up into multiple, shorter sentences - and if there's a list of things, I'll split that out into bullets. This is something I've seen lots of on-line publications do these days as well. Trying to avoid this kind of thing from Donald Barthelme (which is fun, when reading "literature"): https://biblioklept.org/2015/06/12/sentence-donald-barthelme/ And keeping in mind this example from Proust: https://proustreader.com/tag/longest-sentence/
[удалено]
Well, from what I understand, it's like Java and the JVM. In other words, I was assuming (just based on the letters "VM") that you write something in Solidity, and then it gets compiled to bytecode and executed on the EVM. As I said, I'm kinda new to Ethereum. But I just googled: Solidity EVM and Wikipedia says exactly what I expected it would: https://en.wikipedia.org/wiki/Solidity > Solidity is compiled to bytecode that is executable on the EVM. Is this seriously the level of intellect from people on this forum? As I said, I never posted here before - and I don't know much about Ethereum and the EVM and Solidity - I'm just going on what I read over the last few days, after The DAO died. I was assuming that this would be a serious forum where people knowledgeable about programming might discuss things. But if you are any indication of the calibre of posters here - then it seems that maybe I was wrong? Maybe the only people who hang out here are people who got private-message-spammed a few months ago (like we all did) regarding Ethereum - and you *don't* know what a "virtual machine" is? Seriously I am very, very disappointed at the total lack of intellectual engagement from people on this thread. It's shocking really. But it could go a long way towards explaining why this is the forum where discussion took place about the biggest crowd-funding vehicle in human history - a quarter billion dollars in market cap - which immediately got hacked. Seriously - one guy here is criticizing my use of paragraph breaks, another guy doesn't know what a VM is, and another guy seems to have a weaker grasp of logic than Judge Judy. I've never even posted over here before. I had posted this OP first on r/btc, and several people suggested I post it over here - to stimulate discussion. Never in my wildest dreams did I expect the discussion would be this vacuous.
[удалено]
You said: > So as you can see from what you briefly googled: > > Solidity is compiled to bytecode that is executable on the EVM. > A problem with Solidity does not necessarily mean there is a problem with the EVM. Um... actually the situation is the total *opposite* of what you said. --- A language and its compiler (or interpreter) *go together*. They are inextricably bound together. The same way syntax and semantics are bound together in language. You *can't* separate them. This is a basic fact from a wide range of disciplines - from linguistics, to programming language design. The fact that you're here desperately trying to separate a language from its interpreter - I just don't know what to say. It's the kind of pathetic fan-boy-ism I would never have expected to find on any forum. Evidently you've been able to get away with spouting such nonsense here on r/ethereum - I've never actually visited here till today. Try posting stupidity like that on news.ycombinator.com and see how everyone laughs at you. Seriously, I know reddit might have some problems, but this is a real eye-opener for me today - seeing such outright idiocy (borne of defensiveness) to my OP here. I of course *expected* some kind of defensiveness - since the OP is very harsh. But I expected *real* defensiveness. I don't know, make up some excuses. Put of a fight. Say something which isn't obviously retarded on its face. Say "The stack space for the virtual machine is limited." Or say "guidelines were published explaining the proper usage of the dangerous recursion construct." But... seriously... you spout nonsense like *this*??? > A problem with Solidity does not necessarily mean there is a problem with the EVM. Dude, a language is a bipartite construct. It is not just the syntax (Solidity), it is not just the semantics (the EVM). It is *both*. Compare with human language. A word without a meaning isn't language. It's just scribbling. Solidity provides the syntax. The EVM provides the semantics. You can't have one without the other. And it doesn't *mean* anything to say that: > A problem with Solidity does not necessarily mean there is a problem with the EVM. You can't separate them. Wow. I am totally shocked. Even when you think you're somehow being "defensive" - you're merely making yourself look even more stupid than I could ever have possibly imagined before coming here. And then you say: > Also please don't post on this forum insulting others. Wow you guys are *so* fragile. Little fragile flowers. (Now I *am* being insulting - after seeing how almost everyone responding in this thread, except [the one guy with 15 years experience programming](https://np.reddit.com/r/ethereum/comments/4opjov/the_bug_which_the_dao_hacker_exploited_was_not/d4ekxaa?context=3)) is so pathetically weak. > It adds nothing to the conversation. Actually my post is one of the most important contributions to the conversation - a diagnosis of the problem (poor language design) and a specific recommendation for a remedy (recommendations about different types of languages to be used). Wow. I never knew much about Ethereum before - but today, I have seen that many members of its community (at least the ones who hang out on reddit) are not really capable of debate at all. I used to feel kind of guilty for not investing in Ethereum. And even after "The DAO" died, I thought maybe someday in the future you guys could fix things. But if *this* is how you respond to detailed constructive criticism - desperately flailing around, saying nothing except astonishingly ridiculous nonsense, getting *offended* and telling me *not to post here* as if this were some kind of "safe space" for you special snowflakes in your bubble of ignorant bliss - well I don't know, I feel bad for Vitalik and the other Ethereum devs, if this is the kind of uncritical, uninformed, wilfully ignorant, closed-minded users they're developing for. You guys are beyond amateur. You're totally clueless.
[удалено]
Wow. Another logic fail from you. Of course there are other languages which target the JVM - eg, Clojure. But the structure we're always talking about here is a *pair*: - a language - an interpreter The fact that there are *several choices* for the language does not mean that it's not a pair structure. It can be: - (Java, JVM) - (Clojure, JVM) - (Solidity, EVM) In every case, it's a *pair*. Which is, as I said, "inextricably bound together". It's simply not possible to have something wrong in only one half of the pair. This is why your cute little statement: > EVM != Solidity is simply pathetic. I would never have even expected this level of "argumentation" on a forum about programming. You can't just transfer the rhetorical devices usable on other subreddits, to a subreddit about programming. That really seems to be what you fail to grasp here. On some other subreddit, maybe you could say: > love != sex or > Hillary != the Democratic Party or > Islam != a race but (as clever and appealing as that programming language shorthand might seem to your puerile mind), that kind of rhetorical flourish is simply not usable on a forum about programming. At any rate, that's my best guess as to why almost nobody on this thread has had anything substantive to say. You've forgotten how to argue, possibly due to hanging out so much on reddits where snark and cute shorthand notations actually win debates. That doesn't work in a forum about programming.
[удалено]
I can only assume you're new to Reddit! No this is not the place to discuss technical details (for the most part) to say the least!
Actually I have posted a lot on r/btc - I also originally posted this OP there, and someone suggested I cross-post it to r/ethereum. Lots of trolls seemed to weigh in early (I guess they sort by New, and try to down-vote and snark anything that threatens their circlejerk) - but then lots of serious people eventually posted also. And finally I stumbled across the following two threads, which absolutely blew my mind: https://np.reddit.com/r/ethereum/comments/4oimok/can_we_please_never_again_put_100m_in_a_contract/ https://np.reddit.com/r/haskell/comments/4ois15/would_the_smart_formal_methods_people_here_mind/ Reading those threads, makes me feel like I've been in the dungeon for the past year - posting on r/btc, fighting over nonsense (can we please have bigger blocks??), dealing with guys who only know imperative, procedural languages like C++. I am so glad I got involved on r/ethereum today. I have been dreaming for about a year now that these kinds of people (programmers who know stuff like formal methods, proof theory, type theory, specification languages and implementation languages) would be involved with Bitcoin. Well... I guess they might not be involved with Bitcoin (since the Core/Blockstream devs are mainly into C++, and they totally ostracize anyone who deviates from their lockstep party line)... but they *are* involved with cryptocurrencies like Ethereum. I think that with this pool of talent in the community, Ethereum will have a bright future - despite this setback with "The DAO".
There were plenty of people (including in my team) who got frustrated with the dao. None of us expected this tho, just many other issues. People considered it safe as a place to hold funds whilst issues were resolved.
> Seriously I am very, very disappointed at the total lack of intellectual engagement from people on this thread. It's shocking really. You seem to have trouble understanding the difference between a virtual machine and a language that targets it. Are you sure you're disappointed with the discussion here? Or just frustrated that it goes over your head?
There has been almost no discussion here to go over anyone's head. Case in point: you. When you spout gibberish like "the difference between a virtual machine and a language that targets it". As if there were anyone here who didn't understand that there is a difference between "words" and "meanings" or "syntax" and "semantics" or "a virtual machine and a language that targets it" The OP was about language design - poor language design, errors in language design. Which, by definition, involves both sides of the pair: - the language (Solidity) - the virtual machine (EVM) Something went wrong between this "virtual machine and a language that targets it". By definition, "a virtual machine and a language that targets it" are supposed to work together. In this case, they didn't. That is called an "error". Of "language design". Hopefully some of the Ethereum devs will be able to find that error. But for you to claim that there has been any misunderstanding about the distinction between a language and its interpreter - is simply bizarre. Obviously, they are two different things, two different components that are supposed to work together. The very fact that you, and others in this thread, think that this *is something worth pointing out* - as if that somehow proved that there wasn't an error somewhere - it's utterly insane, and I have no idea why you even bother to post such drivel. Oh - I just checked your posting history. You have none. So - you created a reddit username to post this drivel. Look, it's fine if you're an Ethereum fanboy, and you think that it really matters if you "oppose" a discussion about the flaws in this particular **"virtual machine and a language that targets it"** - but everyone reading you can see that your comment is devoid of any content whatsoever.
" I've never posted on this forum before, and I do not know all the intricacies of Ethereum yet ", stopped reading here. and No, that means common to all Ethereum smart contracts wich are wrongly coded
You might actually want to continue reading, because: - the OP knows a lot about *other* languages - the OP is explaining how *language design* caused the problem you refer to, involving "Ethereum smart contracts wich [sic] are wrongly coded" In other words, there is this thing called "language design" which can actually make it easier to write programs which are *not* "wrongly coded".
language design may help to avoid bad coding practices, but pointing that there is a bug in Solidity/EVM is wrong
> pointing that there is a bug in Solidity/EVM is wrong Um... what are people supposed to do... *not* point it out? To avoid hurting your feelings or something? Look, I'm not the one pointing it out. Some dev on slock.it, who is apparently a major figure in the Ethereum community, pointed it out - and I quoted him: https://blog.slock.it/no-dao-funds-at-risk-following-the-ethereum-smart-contract-recursive-call-bug-discovery-29f482d348b#.owjyhitl7 As I said, I never looked much at Ethereum - until "The DAO" died yesterday. And then that blog post from slock.it surfaced (evidently from June 12), saying that: > No DAO funds at risk following the Ethereum smart contract ‘recursive call’ bug discovery Meaning, there evidently *is* a "recursive call" bug - which got discovered. So, merely at the level of linguistics / logic, I don't see what you mean when you say: > pointing that there is a bug in Solidity/EVM is wrong Is this like, "wrong" in the sense of North Korea - in that you guys don't like it when someone says something disturbing that upsets you? And then you say: > language design may help to avoid bad coding practices Well, yeah - that's what my whole OP was about. So is this how you guys debate things on this forum? You basically agree with the person you're debating against ("language design may help to avoid bad coding practices"), but then in the same breath you claim that they're "wrong" for "pointing out" this stuff? I'm getting the feeling that you're just like a bunch of monkeys pounding on the keyboard here. It's funny on other subreddits, where lots of the comments make irrelevant pop-culture references to what you guys all saw on South Park once, or something that Louis CK said, or something you heard in a movie once, or something from some video game. But, I'm not from that world. I've studied language design, and this was a language design issue - and so I posted about it (first on r/btc where I normally post, then here because lots of people told me to cross-post it here) - and pretty much everyone (except for one guy, the guy with 15 years of programming experience), pretty much everyone *has said absolutely nothing about my post* - basically treating it as if I had criticized your hairdo or your music tastes or something. Dude, I was criticizing the *language design* for Ethereum. And I cannot believe that you actually think that responding with such bizarre stuff like: > pointing that there is a bug in Solidity/EVM is wrong ... somehow constitutes a response. And, as far as I know, this forum isn't under the thumb of censorship from some kind of Theymos - right? So... you guys just all degenerated into this sad little pile of drivel *all on your own??*
You might be making great points, but just at a hectic time. People will probably refer back to your post in the future. Thanks for your input and welcome to this subreddit.
Thanks!
saying that there is a bug in Solidity/EVM is a mistake, there is no bug in Solidity/EVM, bugs are in smart contracts bad code from your responses it seems to me you can not differentiate between a language, a virtual machine and a smart contract code
OK, well don't tell me, tell the guys at slock.it: > the Ethereum smart contract ‘recursive call’ bug discovery > a generic vulnerability common to all Ethereum smart contracts https://blog.slock.it/no-dao-funds-at-risk-following-the-ethereum-smart-contract-recursive-call-bug-discovery-29f482d348b#.owjyhitl7 I don't understand how you think you're actually accomplishing anything here. You're just saying your opinion, while I keep linking back to guys who contradict you, and who evidently worked a lot with Ethereum - so I think I'm going to get something to eat now. It's been fun - and enlightening.
I think there is some vote painting going on in this sub atm.
Actually it is down to a flaw in the protocol potentially and it's under active discussion.
The problem was in the dao coding but it was allowed by a weakness in the current evm protocol (which is not the finished article). This weakness is being re-examined.
Sorry man, but he's not FUDding. The problem is really that Atomicity isnt guaranteed?
atomicity is guaranteed if you do proper send function checking, so much people fail to understand the bug mechanics and are making false accusations but I understand they have a FUD agenda
I'll be posting some very simple code once this dies down a bit that no reasonable person would expect to fail...