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

Ask HN: What is your favorite CS paper?

news.ycombinator.com

Post reply on HN
Print view View original

41–50 of 265 posts

Re: Ask HN: What is your favorite CS paper?

#42

Post by LeanderK »

jasode wrote: post #17

"The Limits of Correctness" (1985) by Bryan Cantwell Smith: https://www.student.cs.uwaterloo.ca/~cs492/11public_html/p18... I know Thompson's "Reflections on Trust" and Shannon's "Communication" papers are more famous but I believe BCS's "Correctness" paper has more immediate relevance to a wider population of programmers. For example, I don't believe Ethereum's creator, Vitalik Buterin, is familiar with it because i…

i enjoyed skimming the paper, but i don't agree to your conclusions. It reminds me of an recent discussion i had about Dependent Types in Haskell, why not just check for termination instead of asserting it (I know about the halting problem)?

I think for many applications there is no binary answer, it's not just a good or bad idea. The question is how good can we get and is it any better than the state of the art? There are theoretical limits, but the interesting part is whether there exists a practical approximation. I don't believe in a fundamental difference between us and computers, i think everything we can reason about should be possible to algorithmically reason about. I think smart-contracts are a fundamental improvement over "non-code as law", i really believe in them. They are reproducible and exact. But it's a shame that solidity is so badly engineered, because they it is really hard to prove anything in it. I think they did the exact opposite of what would be the right language. I understand the reasoning behind "the limits of correctness", but does this means that proving anything is meaningless?

I would expect most contracts to be stupidly simpel, at least to a machine, with simpel properties that need to be proven comparable to testing Haskell with quickcheck. And i believe they are an improvement over "non-code as law", even if not provably correct.

The problem with bugs and smart-contracts is interesting. But implementing smart-contracts does not mean automating the judge.

Re: Ask HN: What is your favorite CS paper?

#47

Post by tom_mellior »

throwawayjava wrote: post #40
catnaroek wrote: post #26

Earlier quoted context omitted.

> you will see that the DAO hack and its reversal as inevitable. Honest naïve question. What's the proof?

FWIW I think this is a very fair question. Parent's post veers a bit further toward defeatism than I think Smith's paper advocates for or justifies. In particular, of course the DAO hack wasn't inevitable -- a more careful programmer could've foreseen and prevented that attack and whole other classes of attack.

Part of the linked paper's point is that because computer systems involve many "levels of failure", even a more careful programmer cannot usually rule out every class of programs. The DAO hack, yes, possibly.

But, for example, people have also lost money due to bugs in the Solidity compiler: https://np.reddit.com/r/ethtrader/comments/5foa5p/daily_disc... How many "more careful" Ethereum programmers also check the compiler for correctness?

Another paper in this vein is James Fetzer's "Program Verification: The Very Idea". http://lore.ua.ac.be/Teaching/SSPEC2LIC/critique2.pdf

Re: Ask HN: What is your favorite CS paper?

#49

Post by tom_mellior »

efferifick wrote: post #21

Producing Wrong Data without Doing Anything Obviously Wrong. Immediately useful for anyone measuring compiler transformations performance!

Great paper, yes. Immediately useful? More like disheartening, because it doesn't really tell you how to be sure your measurements are OK.
Post reply on HN