Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Deconstructing the DAO Attack: A Brief Code Tour

vessenes.com

Post reply on HN
Print view View original

161–167 of 167 posts

Re: Deconstructing the DAO Attack: A Brief Code Tour

#161

Post by egg_head »

whazor wrote: post #67
tinco wrote: post #37

In addition to this the language is not explicit enough. Even standard Haskell wouldn't be safe enough for a program that manages $250MM directly without safe guards. In addition to typesafety, it would have to be both explicitly typed at the lowest possible granularity and annotated with pre and post conditions. Not only did this code allow a bunch of tokens be transferred without compensation, it left the whole acc…

To counter your attack on Buterin, he is aware that writing safe contract code requires proofs and type safety. That is why solidity is compiled to EVM code, so that improved languages could incorporate this. Solidity is built for rapid innovation and user friendliness. Buterin is now more busy with sharding and scaling issues.

When I had my own start up companies or worked for those of my friends, we ensured that the first few sets of big customers got white glove treatment from the executive team....

This is what happens when one does not do that. :)

Re: Deconstructing the DAO Attack: A Brief Code Tour

#162

Post by bzbarsky »

jacquesm wrote: post #2

Whoever thought it was a good idea to have case sensitive function names where the names are allowed to be identical but not identical in function? Major fuck-up there. That should have never passed the concept stage, nor the review stage. Function names should describe what a function does.

For any language that allows non-ASCII identifiers, trying to define "case insensitive" is a minefield best avoided. For example, with general Unicode characters, "case-insensitive" comparison doesn't give you an equivalence relation on identifiers because transitivity fails.

Of course you can define things to be case-insensitive only in the ASCII range, and treat your non-ASCII stuff as second-class citizens...

Re: Deconstructing the DAO Attack: A Brief Code Tour

#164

Post by willtim »

pron wrote: post #139
willtim wrote: post #138

Earlier quoted context omitted.

> When are Turing machines ever involved? Most software is written in imperative Turing equivalent languages, so Turing Machines are involved all the time. The fact that most verification software is not capable of dealing with them, demonstrates a language issue. Which is the point I have been trying to make. > It isn't. Logic was applied to programs long before FP was in vogue. I'm advocating modelling contracts wi…

> Most software is written in imperative Turing equivalent languages, so Turing Machines are involved all the time. I don't understand what that means. Everything is "Turing equivalent" in some sense[0]. It's like saying that since every language can be compiled to C, then C is "involved all the time". That would even be more accurate, because our programs are most certainly not TM-equivalent. Proof: the asymptotic c…

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

Re: Deconstructing the DAO Attack: A Brief Code Tour

#165

Post by baby »

jsprogrammer wrote: post #136
kartickv wrote: post #135

Earlier quoted context omitted.

Which is irrelevant, since languages are a medium of human expression, not a way to store bits on the disk.

Irrelevant to what? The two words literally are represented with different bits (code).

Assuming you are not trolling: yes they are indeed represented with different bits, which doesn't matter since these bits are not the bits executed by the CPU in the end. The "words" and not the bits are interpreted or compiled into machine code. Which is where bits matter.

Re: Deconstructing the DAO Attack: A Brief Code Tour

#166

Post by codingmyway »

semi-extrinsic wrote: post #110
buttershakes wrote: post #11

Earlier quoted context omitted.

I couldn't agree more with this sentiment. I haven't spent too much time on Ethereum contracts but this is such a ridiculous language/platform design issue.

Funny thing is, it reminds me of implicit typing of int/float based on the first letter of the variable name that ye olde FORTRAN77 had as a major footgun.

Upvoted for introducing me to the word footgun

Re: Deconstructing the DAO Attack: A Brief Code Tour

#167

Post by pron »

willtim wrote: post #164
pron wrote: post #139

Earlier quoted context omitted.

> Most software is written in imperative Turing equivalent languages, so Turing Machines are involved all the time. I don't understand what that means. Everything is "Turing equivalent" in some sense[0]. It's like saying that since every language can be compiled to C, then C is "involved all the time". That would even be more accurate, because our programs are most certainly not TM-equivalent. Proof: the asymptotic c…

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

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