TE
TechEcho
Home24h TopNewestBestAskShowJobs
GitHubTwitter
Home

TechEcho

A tech news platform built with Next.js, providing global tech news and discussions.

GitHubTwitter

Home

HomeNewestBestAskShowJobs

Resources

HackerNews APIOriginal HackerNewsNext.js

© 2025 TechEcho. All rights reserved.

Vigorous Public Debates in Academic Computer Science

81 pointsby madover 8 years ago

8 comments

Animatsover 8 years ago
Some of those are classics. The Lipton-Perlis-DeMillo argument against program verification is a good one.[1] They demonstrated that manual programming verification via hand theorem proving is buggy. Automated theorem proving was new back then.<p>This was an issue back in the 80s for a philosophical reason in mathematics. Mathematics classically approves of short, clever, elegant proofs. The paper-and-pencil crowd was trying to do that for code. In practice, program verification is about mechanized grinding through massive numbers of dumb assertions to catch off-by-one errors.<p>This used to bother mathematicians. When the four-color theorem was originally proved, it was done partly by hand and partly with computer case analysis. The computer part bothered many mathematicians. The culture has changed. Recently, someone redid the proof with the old hand parts re-done by computer. Since that eliminated some possible human errors, that was a step forward in solidifying the proof.<p>We also know now how to check a theorem prover. Some theorem provers emit a proof trace, huge files of &quot;Step 2437: apply rule 42 to change 2*X to X+X&quot;. Proof traces can be fed into a dumb proof checker which does the indicated rewrite and checks that the expected output is obtained.<p>So progress has resolved that issue.<p>[1] <a href="http:&#x2F;&#x2F;www.yodaiken.com&#x2F;papers&#x2F;p271-de_millo.pdf" rel="nofollow">http:&#x2F;&#x2F;www.yodaiken.com&#x2F;papers&#x2F;p271-de_millo.pdf</a>
评论 #12624864 未加载
评论 #12623848 未加载
评论 #12623827 未加载
pronover 8 years ago
While not exactly a debate -- more of a fundamental difference in outlook -- these are interesting, completely opposite claims:<p>Bob Harper[1]:<p>&gt; There is an alternative… without… reference to an underlying machine… [W]e adopt a linguistic model of computation, rather than a machine model, and life gets better! There is a wider range of options for expressing algorithms, and we simplify the story of how algorithms are to be analyzed.<p>Leslie Lamport[2]:<p>&gt; Thinking is not the ability to manipulate language; it’s the ability to manipulate concepts. Computer science should be about concepts, not languages. … State machines… provide a uniform way to describe computation with simple mathematics. The obsession with language is a strong obstacle to any attempt at unifying different parts of computer science.<p>[1]: <a href="https:&#x2F;&#x2F;existentialtype.wordpress.com&#x2F;2011&#x2F;03&#x2F;16&#x2F;languages-and-machines&#x2F;" rel="nofollow">https:&#x2F;&#x2F;existentialtype.wordpress.com&#x2F;2011&#x2F;03&#x2F;16&#x2F;languages-a...</a><p>[2]: <a href="http:&#x2F;&#x2F;research.microsoft.com&#x2F;en-us&#x2F;um&#x2F;people&#x2F;lamport&#x2F;pubs&#x2F;state-machine.pdf" rel="nofollow">http:&#x2F;&#x2F;research.microsoft.com&#x2F;en-us&#x2F;um&#x2F;people&#x2F;lamport&#x2F;pubs&#x2F;s...</a>
评论 #12624158 未加载
评论 #12628805 未加载
评论 #12623957 未加载
tlbover 8 years ago
I was a co-author on one of the contentious papers [0] in log-structured file systems, addressing the question of whether log cleaning could be done during idle times (yes, for any reasonable workload).<p>There was a surprising amount of drama and personal rivalry. While distracting, knowing that our results would be picked apart motivated us to be really rigorous.<p>In the end, modern file systems take the best aspects of both. Like the RISC-CISC debate, it&#x27;s hard to draw a firm conclusion about the two ideas because they&#x27;re tied up with the quality of implementations, and the optimal answer involves a synthesis of the ideas.<p>[0] <a href="http:&#x2F;&#x2F;www.eecs.harvard.edu&#x2F;margo&#x2F;papers&#x2F;usenix95-clean&#x2F;paper.pdf" rel="nofollow">http:&#x2F;&#x2F;www.eecs.harvard.edu&#x2F;margo&#x2F;papers&#x2F;usenix95-clean&#x2F;pape...</a>
userbinatorover 8 years ago
One debate that I thought would be mentioned is &quot;Goto statement considered harmful&quot;, &quot;&#x27;GOTO Considered Harmful&#x27; Considered Harmful.&quot;, and &quot;GOTO Considered Harmful&quot; Considered Harmful&#x27; Considered Harmful?&quot; I think it&#x27;s somewhat disappointing that a lot of CS education always mentions Dijkstra&#x27;s original argument, but not the other side. The latter two can be found here:<p><a href="http:&#x2F;&#x2F;web.archive.org&#x2F;web&#x2F;20090320002214&#x2F;http:&#x2F;&#x2F;www.ecn.purdue.edu&#x2F;ParaMount&#x2F;papers&#x2F;rubin87goto.pdf" rel="nofollow">http:&#x2F;&#x2F;web.archive.org&#x2F;web&#x2F;20090320002214&#x2F;http:&#x2F;&#x2F;www.ecn.pur...</a><p><a href="https:&#x2F;&#x2F;dx.doi.org&#x2F;10.1145%2F22899.315729" rel="nofollow">https:&#x2F;&#x2F;dx.doi.org&#x2F;10.1145%2F22899.315729</a>
评论 #12623929 未加载
评论 #12623817 未加载
评论 #12624514 未加载
评论 #12623306 未加载
评论 #12631269 未加载
评论 #12623521 未加载
westoncbover 8 years ago
I had heard vaguely of the &#x27;microkernal debate&#x27; in the past, but never checked it out. Didn&#x27;t realize the other main participant (aside from Linus Torvalds) was Andrew Tanenbaum. Very entertaining&#x2F;interesting read. (The linked article refers us here: <a href="http:&#x2F;&#x2F;www.oreilly.com&#x2F;openbook&#x2F;opensources&#x2F;book&#x2F;appa.html" rel="nofollow">http:&#x2F;&#x2F;www.oreilly.com&#x2F;openbook&#x2F;opensources&#x2F;book&#x2F;appa.html</a>)
评论 #12623154 未加载
tr352over 8 years ago
To be fair, these are debates about issues that are rather insignificant from a broader CS perspective. Engineering problems (methodology, network protocols, file systems, kernel implementation details) or debates that are infamous mostly due to their polemic nature (Dijkstra-Backus, or Dijkstra-Anything, for that matter).<p>I think it&#x27;s true. In CS there are no deep fundamental or philosophical debate-evoking schisms of the likes you sometimes find in other fields. Consider economics, philosophy, physics (theory of everything) or the soft sciences.<p>Even the hottest problem in CS (P vs NP, of course) doesn&#x27;t seem to evoke much debate among computer scientists.
评论 #12624269 未加载
jackmottover 8 years ago
Need a lot less rhetoric and a lot more controlled experiments.
评论 #12624696 未加载
评论 #12623912 未加载
GFK_of_xmaspastover 8 years ago
Also of interest is one of regehr&#x27;s commentators posting a link to Kahan&#x27;s rebuttal to those &quot;unum&quot; numbers.