Vigorous Public Debates in Academic Computer Science(blog.regehr.org) |
Vigorous Public Debates in Academic Computer Science(blog.regehr.org) |
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.
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.
We also know now how to check a theorem prover. Some theorem provers emit a proof trace, huge files of "Step 2437: apply rule 42 to change 2*X to X+X". Proof traces can be fed into a dumb proof checker which does the indicated rewrite and checks that the expected output is obtained.
So progress has resolved that issue.
https://www.cs.utexas.edu/users/jared/milawa/Web/
They start with small logics you can do by hand in verified code. They gradually build on them, one layer at a time, increasingly sophisticated logics until they have a useful theorem prover in first-order logic. I also found a HOL-to-FOL converter. Since most of their stuff is HOL, that means we're almost done at that point for the verification chain.
http://research.microsoft.com/en-us/um/people/lamport/pubs/l...
Bob Harper[1]:
> 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.
Leslie Lamport[2]:
> 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.
[1]: https://existentialtype.wordpress.com/2011/03/16/languages-a...
[2]: http://research.microsoft.com/en-us/um/people/lamport/pubs/s...
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.
In the end, modern file systems take the best aspects of both. Like the RISC-CISC debate, it's hard to draw a firm conclusion about the two ideas because they're tied up with the quality of implementations, and the optimal answer involves a synthesis of the ideas.
[0] http://www.eecs.harvard.edu/margo/papers/usenix95-clean/pape...
http://web.archive.org/web/20090320002214/http://www.ecn.pur...
https://web.archive.org/web/20050514121653/http://www.eros-o...
https://web.archive.org/web/20050211090602/http://www.eros-o...
Two other good articles are why the EAL4 evaluations that Windows et al were getting are worthless and what a secure, build system might look like.
https://web.archive.org/web/20040214043848/http://eros.cs.jh...
https://www.usenix.org/legacy/publications/library/proceedin...
I think it'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.
Even the hottest problem in CS (P vs NP, of course) doesn't seem to evoke much debate among computer scientists.
For example: someone in nineties-or-naughties once experimentally "proved" that Java was faster than C for matrix maths -- because of the overhead of `free()`! If that sounds ridiculous to you, then understand this really matters for certain implementations of certain matrix problems.
So the take-away hangs not on the nature of C vs. Java, but on whether the study matters in the real world. Emprics in CS are good for engineers quietly doing their own job, but for debates they are as fraught as in the soft-sciences.
Indeed CS is a soft-science. Or rather it is not a science at all, but a mathematical art, with bonus people issues.
Current languages mostly don't even allow the bad kinds anymore, so people can ignore history, and complain that "goto isn't so bad, I've never seen anybody abusing it like he claims in the essay."
But we do teach them that. As a result I recently had to review changes made by a (very capable) junior colleague who failed to actually implement the desired feature, but did get so upset by the goto-based error handling that he replaced it with incorrect exception-based code.
The empirical approach would be to compare outcomes of different approaches, trying to control the independent variables.
But CS instead seems to be run by polemic, "Well, obviously..." rhetoric, and tribal affiliation.
I've yet to be convinced this is the ideal way to improve the tools and techniques of CS.
(https://m.facebook.com/story.php?story_fbid=1015411943840422...)
Langsec is a notable exception where Chomsky's hierarchy paid off big time. The notations and implementations still more consistent with Lamport, though. So, semi-exception.
When teaching a language that support bad gotos, or compilers. Otherwise, you can count a lot of people (including me) out of that undefined "we" pronoun.
There's little point in teaching newbies about goto at all. The few modern implementations are for experts, because it can still lead to some bad code, just not the kind of "bad" Dijkstra was talking about. Yet there's a group of people that will evangelize about any subject you can think about, normally people with very shallow knowledge on the subject.
People usually present his work in terms of proofs only. Typically with big O considerations. Reading him, he very quickly warns of the dangers in big O analysis. (He is still a fan of it. Encouraged it as a math aid for grade school work, at one point.)
Do you have a link / some elaboration?
But TL.DR. - He got digged plenty of repeating cases of bad code, and proceeded to fix every one of them with very few coherent and systematic changes.
1 - His notes are here: http://www.cs.utexas.edu/users/EWD/ unfortunately, I don't remember what numbers to look.