Edsger Dijkstra – The Man Who Carried Computer Science on His Shoulders
inference-review.com
inference-review.com
Years later, in grad school, my research was on program verification. Dijkstra was a big influence on the field. I attended a lecture at UT Austin that he gave before moving to the US.
Dijkstra's approach to proving the correctness of programs is hard to apply in practice. Like a geometry proof, there are ways in which a proof of correctness can have mistakes that aren't obvious. Here's an example, prove that a sorting algorithm works. If the specification is that the output must be in sorted order, a proven program can still fail to sort correctly. The specification has an error, the output must not only be in sorted order, it must ensure that all of the input elements make it somewhere to the output. But this isn't good enough. A sort proven to meet this specification might leave out some duplicate values. Requiring that the output be the same length as the input still isn't good enough, multiple copies of one element might hide missing duplicate input values for another element. The specification requires that the output be a sorted permutation of the input.
Sorting is a well understood problem, but real verification must deal with the strange mathematics implemented by computers. The mathematical theories that we are accustomed to from school assume infinite precision and no overflow, real life hardware doesn't act this way.
All of this makes program verification hard, and my hope is that AI programming assistants will someday aid in the construction of meaningful specifications and work with the programmer to verify the correctness of programs or determine their safe operating boundaries. Progress has been slow, and the tools are still impractical for use by most programmers on most programs.
There’s no checking to see if your specification is under-specified.
This submission from yesterday may interest you.
Given what I've seen of AI today (works reasonably well at the best of times, but is sensitive to unusual cases and can produce totally nonsensical results otherwise; and nearly impossible to actually debug), I remain highly skeptical.
Bugs can still occur of course, but if one restricts oneself to valid manipulations the bugs will be found in the specification and reflected in the code. It's not a magic bullet, and that's one of the reasons TLA+ was invented, it helps with complexity on the specification side. However a method like the one Dijkstra shows in the referenced paper can be used to faithfully implement the TLA+ checked specification.
He wouldn't even get in an university to get the chance to be fired. And that's not specific to the US, it applies to nearly all developed or developing countries.
That person wouldn't be able to get much past a PhD, even as a student.
Also, by some miracle you manage to graduate by minimal publishing or no publications you will find all doors to getting research funding shut. This means that you are basically unemployable as a tenure track professor (universities prefer their newly minted assistant professors to come with funding).
http://www.netlib.org/bibnet/authors/d/dijkstra-edsger-w.htm...
(The ones marked "circulated privately" are the EWD series.)
There was a feel on campus that the people who were really going to 'make it' were only putting in B- or C+ work and spending the rest of their time working on side projects. There were very few days in a given year when more than half of the computer labs were full at the same time, and with Unix boxes you can always remote in to the flavor of machine you need.
You don't need much research budget if you already have access to time on equipment. I'd be curious to know if Dijkstra had access to a similar embarrassment of riches.
Dijkstra spent a good chunk of the latter part of his career at the University of Texas in Austin. There was plenty of access to facilities there, but that wasn't really what his research was about. He wrote longhand (scans here: https://www.cs.utexas.edu/users/EWD/) and didn't really use much technology directly in his work.
This makes sense, because after all, Dijkstra is responsible for this famous quote: "Computer science is no more about computers than astronomy is about telescopes".
https://www.quora.com/What-did-Dijkstra-mean-when-he-said-Co...
I remember some of my classmates were turned off by how theoretical some of the core courses were. A lot of people saw it as less practical. Also the height of Java's OO take over of CS programs, it was definitely a mix of classes. Although the theory courses tended to either care less about language choice or focused on Haskell.
And the vast majority of people who graduate with a CS degree are going to work as software engineers, not as computer scientists. They are therefore being mis-educated to the degree that their CS program agrees with Dijkstra's philosophy. (Which doesn't mean that Dijkstra is wrong about CS. It just means that a CS degree shouldn't be the passport to a career in software engineering, or even a job as a grunt programmer.)
Second, I suspect (but cannot prove) that this problem is why computer science grads need a couple of years of close supervision on the job before you can trust them with anything.
It is and it isn't. Most degree programs don't require it, and some don't integrate it as a for-credit option, but most (including in the sciences) do open opportunities for them, and lots of students take advantage of that opportunity and are more employable because of it.
But it is my position that a graduate of a proper software engineering degree would take less initial supervision than a graduate of a CS degree.
Why? Because they would have already seen ambiguous requirements, and would have an idea of what to do. They would have already seen a multi-hundred-thousand-line code base, and would be more likely to have some idea how to navigate in one. They would have some idea of what production-level code looks like, and how to go about achieving that level of completeness. And so on.
There's more to it than that, a lot of which has more to do with learning how companies are structured and how people communicate in the corporate world. Among other things, college students have been trained to tackle any assignment with the assumption that the information they have been given is accurate and comprehensive, and the professor would prefer to hear nothing from them until the assignment is turned in as complete as possible right before the deadline.
If you want to educate people to be immediately productive in a corporate environment, that's not what college is for anyway.
Not sure what they're doing today.
UTCS 1997 here. I've been employed in software-related industries continually since graduation, and I can honestly say my UTCS degree has been nothing but helpful in that regard.
BTW, the personal website listed in your profile is down. You might want to look into that.
Furthermore, there really is two kinds of CS departments: the ones that were spun out of a Math department and those that emerged out of an Electrical Engineering one.
Eventually, he got a Macintosh (IIRC, Cynthia Matuszek (https://www.csee.umbc.edu/~cmat/) was the one who set it up for him. (Hi!))
Moishe Lettvin - What I Learned Doing 250 Interviews at Google. It is on Etsy Eng channel Youtube url with the relevant time frame https://youtu.be/r8RxkpUvxK0?t=532
Here is Freeman Dyson; the Physicist without a PhD ( https://www.quantamagazine.org/a-math-puzzle-worthy-of-freem... );
Oh, yes. I’m very proud of not having a Ph.D. I think the Ph.D. system is an abomination. It was invented as a system for educating German professors in the 19th century, and it works well under those conditions. It’s good for a very small number of people who are going to spend their lives being professors. But it has become now a kind of union card that you have to have in order to have a job, whether it’s being a professor or other things, and it’s quite inappropriate for that. It forces people to waste years and years of their lives sort of pretending to do research for which they’re not at all well-suited. In the end, they have this piece of paper which says they’re qualified, but it really doesn’t mean anything.
- B.S. = bull shit
- M.S. = more shit
- PhD = piled higher & deeper
She's a happy software tester now :-)
Unfortunately there was a huge gap in what was expected of these people and what they could actually do. Save but a few they were pretty awful employees for the job. Not necessarily their fault, but it's one example of the gamification of the system.
And if you think an oversaturated job market pushing people into doing PhD's they don't need for the actual job isn't a problem for "the PhD system" then I call you short sighted.
It might be different in Process Chemistry, which is where the best lab work is work. Perhaps those who have the magic in scaling up a reaction into production are like those who can debug anything? I've never worked with those groups or with the Analytical chemists in Development.
Disclaimer: I have a PhD, but never wished to go into academia due to the politics. And yeah, it's a union card.
I don't know which country GGP (or his wife) is from, and you might well be correct about your assessment, but there are some countries where master's degrees are viewed differently than in the U.S.
Where I live and did my degree (Northern Europe), it's commonplace to do a master's rather than just a bachelor's degree. In fact, in many fields the master's used to be considered the basic "undergrad" degree here. A bachelor's degree existed, but in many fields you'd have been considered to have dropped out of completing a master's if you only had bachelor's. That might be slowly changing, with a higher emphasis given to bachelor's level degrees, but the sentiment probably still remains.
> (waste years and years of their lives) sort of pretending to do research for which they’re not at all well-suited
Suggesting that incentives to do research that follows academic tradition do not aligign with the best possible outcomes of independent investigation.
Which is what we both point out.
Having one in CS myself U can assure you are right for the IT field. Getting this PhD was about personal aspiration rather than career success.
Definitely not! It is a philosophical paper.
That said, I don't know about self-mockery. A good line from the linked lecture transcript:
> The competent programmer is fully aware of the strictly limited size of his own skull; therefore he approaches the programming task in full humility, and among other things he avoids clever tricks like the plague.
He seems to be addressing the issue of inflated egos influencing people to be "real programmers". For example, do you use a simple GUI interface? -- HA! I can type an arcane string into a command line with my TOES! Clearly, I art teh superior to thou. Which is stupid, because a proper GUI that shows the full scope of the API is awesome, while memorizing arcane strings is a silly practice. But, some folks let feelings of intellectual superiority cloud their judgement and beliefs, which Dijkstra was speaking out against.
He repeats this theme several times, with the overall lecture being a tad repetitive and redundant as it states the same thing over and over in a repetitive series of repetitions, but for a specific example:
> Finally, although the subject is not a pleasant one, I must mention PL/1, a programming language for which the defining documentation is of a frightening size and complexity. Using PL/1 must be like flying a plane with 7000 buttons, switches and handles to manipulate in the cockpit. I absolutely fail to see how we can keep our growing programs firmly within our intellectual grip when by its sheer baroqueness the programming language —our basic tool, mind you!— already escapes our intellectual control. And if I have to describe the influence PL/1 can have on its users, the closest metaphor that comes to my mind is that of a drug.
In short, Dijkstra strongly advocates intellectual minimalism. The "humility" he advocates is fortitude against ego-driven peacockery in decision-making; taking the simplest possible approach, that's the easiest to do, even when doing so doesn't show off one's intellect.
A simple solution does not look like much because it is so simple, but it can take a genius to come up with it. Whereas complicated solutions are easier to come by and do demonstrate your intellectual skills.
Just because a person can write code that only they can understand does not mean they are more intelligent than others, nor that the quality of such code would be "good". :-)
The problem with category theory, as I see it, happens due to a mismatch with our mode of creating. We tend to converge in our solutions from chaos to order. Formal systems don’t provide space to be chaotic in. We need to be right the first time.
We need languages and IDEs that will help us find abstractions. Static analysis saying: “this thing here is like all those other things if only you see it like so. Perhaps you want to structure it like those other things as well?”
According to the article, as a young researcher, he was
* A "programmer" (something like a research assistant, perhaps?) at the Mathematisch Centrum (Mathematical Centre) in Amsterdam.
* Professor in the mathematics department of the Eindhoven University of Technology from 1962-1973. (As I understand, the "external funding" thing is less of a problem in mathematics. Also, I have no idea how tenure works there.)
* Finally, research fellow at the Burroughs Corporation.
It's true, he didn't have many direct PhD students (two?!), but his collaborations were many. (I don't know if the Tuesday Morning Group at UT is still active,[1] but it was rather well known and its members produced a great deal of what is now "theoretical computer science".)
If you're trying to compare Dijkstra to J. Random Young Researcher, J's gonna have a hard time any way you look at it.
[1] UT no longer requires automata theory or formal logic for CS undergraduates. They're dead to me.
*Tuesday Afternoon Club [0].
[0] https://www.cwi.nl/about/history/e-w-dijkstra-brilliant-colo...
It says something about me that I get them confused.
Back then, i think full professors were appointed by the Queen. (Certainly so for Beatrix, but he became a prof before her inauguration)
Being appointed by the Queen made it really difficult to fire you - one of the reasons (I was told) they stopped this practice.
Moreover, back then research funding worked very different from how it works now in .nl. Actually, I have some idea of how finding worked from the mid-90s on... but I've read that prior to early 80s, in .nl, most PhD students were part-time and not employed by the university.
Not sure how accurate that is. Irrespective of its accuracy, it's clear that academic life had changed drastically since then. (In .nl at least)
Monarchies today being at that awkward stage where they wield enough protection to prevent somebody from being fired but no longer enough power to get them beheaded…
"It is practically impossible to teach good programming to students that have had a prior exposure to BASIC: as potential programmers they are mentally mutilated beyond hope of regeneration."
The problem is it's quoted regardless of how much the BASIC dialect being discussed resembles the one he was talking about [1]. There are lots of good BASIC languages out there running all kinds of useful software that are dismissed out of hand by a subset of developers simply from that comment.
[1] https://programmingisterrible.com/post/40132515169/dijkstra-...
I've since become quite proficient in C, Ruby, Java, Kotlin, HTML, JS, shell scripting, and many many other languages and environments. So IMO there is very little modern merit to the idea that exposure to BASIC (or any other mocked language) is "mentally mutilat[ing]".
I've yet to meet somebody who got interested in computers through correctness proofs.
In _Coders at Work_, Knuth offers a counter-argument that I find compelling:
> Seibel: It seems a lot of the people I've talked to had direct access to a machine when they were starting out. Yet Dijkstra has a paper I'm sure you're familiar with, where he basically says we shouldn't let computer-science science students touch a machine for the first few years of their training; they should spend all their time manipulating symbols.
> Knuth: But that's not the way he learned either. He said a lot of really great things and inspirational things, but he's not always right. Neither am I, but my take on it is this: Take a scientist in any field. The scientist gets older and says, "Oh, yes, some of the things that I've been doing have a really great payoff and other things, I'm not using anymore. I'm not going to have my students waste time on the stuff that doesn't make giant steps. I'm not going to talk about low-level stuff at all. These theoretical concepts are really so powerful-that's the whole story. Forget about how I got to this point." I think that's a fundamental error made by scientists in every field. They don't realize that when you're learning something you've got to see something at all levels. You've got to see the floor before you build the ceiling. That all goes into the brain and gets shoved down to the point where the older people forget that they needed it.
> Peter Seibel. _Coders at Work_
It is clear from the reading the EWDs that Dijkstra considered actually doing something with Computers detrimental to the practice of Computer Science as he conceived it, but the kind of Computer Science he practiced past 1975 or so was not particularly useful to Computer Engineering, because it refused to engage with it, and, as the article points out, it was not even particularly good math, because it refused to engage properly with that field as well.
Nevertheless Hamiltons software put a man on the the moon.
https://www.cs.utexas.edu/users/EWD/transcriptions/EWD08xx/E...
He made significant, important contributions. He wasn't the only one. Hoare, Backus, McCarthy... there were a lot of people who made important, fundamental contributions.
Structured programming caught on. Proofs did not, for reasons that would have offended Dijkstra - they took time, and it was actually more valuable (both socially and financially) to produce mostly-working software quickly than to produce proven-correct software slowly.
But he never would have accepted that the real world was that way. He insisted that his approach was correct. As Backus said of him, "This guy’s arrogance takes your breath away."
So: Important contributions? Absolutely. More than anyone else's? Perhaps. Carried computer science on his shoulders? No, but he probably thought he did.
He was very likely too much ahead of his time on that. Decades after him we still don't have good enough tech to do the kinds of proof he expected... And yes, maybe too arrogant to realize that it's not the entire world that is dumb, but it's a core piece of the system that is missing.
On the other hand, he did work to improve proof systems, so who knows what he really thought?
Can anyone explain how this "much more complex" recursion works?
[0] https://vanemden.wordpress.com/2014/06/18/how-recursion-got-...
It is Dijkstra's generalizing style which stands out when a comparison is made with the work of his contemporaries. Rutishauser, for example, had limited the order of his procedure activations in his run-time system [59], while Dijkstra had no such restriction. Floyd's work [60, p.42-43] relied on three specialized “yo-yo” lists (i.e., stacks) instead of one general stack. Likewise, the MAD translator [61, p.28] used several specialized tables. Also, and most importantly, the ALCOR compilers were severely restricted in that they could not handle several ALGOL60 language constructs, including the recursive procedure (cf. Section ). Finally, though the Irons-Feurzeig system [54] did implement recursive-procedure activations and by means of one general run-time stack, it was, in the interest of efficiency, sophisticated in its run-time capabilities and, hence, unlike the run-time system of Dijkstra and Zonneveld .
They wanted performance on par with existing languages that didn’t allow recursion, and could simply assign fixed addresses to all function arguments and local variables.
Lisp didn’t have that. It allocated environments left and right. That meant that a function call allocated memory and potentially could trigger garbage collection.
The major improvement was to use a runtime stack. That was fairly novel. Earlier compilers used a stack at compile time to make it possible that those fixed addresses for arguments and locals could be shared between functions that didn’t call each other, directly or indirectly, but that stack didn’t exist at runtime.
And yes, the idea of a stack seems trivial nowadays, but it wasn’t at the time. Quite a few CPUs didn’t even have “jump to subroutine” or “return from subroutine” instructions.
Algol’s “call by name” feature also may have complicated this, but I don’t see how that’s more difficult than passing lambdas as arguments.
I guess they do escape analysis and where items are provably local, stack allocate them. If not, plonk them on the heap.
A call frame is an object like any other, so they go on the heap. This allows you to create closures.
“Dijkstra’s quest to generalize led him to use the well-known concept of a stack (i.e., a continuous portion of computer memory) as a run-time object, rather than a mere compile-time object as was the case in Samelson and Bauer’s ALCOR compiler.”
Digging deeper, I found https://www.illc.uva.nl/Research/Publications/Reports/MoL-20... (worth reading, IMHO) which indicates Samuelson and Baur used a stack to parse expressions and generate machine code for them, not for assigning memory locations.
So, I agree with you it can’t have been as simple als I implied.
I doubt they would have plonked anything on the heap, though, because languages of the time didn’t have a heap (FORTRAN certainly didn’t), and the language Samuelson and Baur wrote didn’t even allow functions to call other functions.
Moving to a stack costs, in that you can't do some things, per my original comment. You gain efficiency for what you can do though.
> used a stack to parse expressions and generate machine code for them
Prob this https://html.duckduckgo.com/html?q=dijkstra%20shunting%20yar... which I thought came from dijkstra but your digging suggests not, didn't know! (edit: it did https://en.wikipedia.org/wiki/Shunting-yard_algorithm) infix -> rpn which matches a stack very well (can evaluate as an interpreter, or emit code as a compiler. Not very efficient but it works).
Edit: much credit for digging and reading before posting, wish I could give you several upvotes for that.
I made lisp-interpreter and toyed with compiler.
It's a bit like parsing, these days we either reach for a technique (eg. recursive descent) or an implementation of a tool (such as flex/bison) and never think there was a time before these where people had to struggle conceptually with these things.
Dynamic scoping is easier to implement than lexical scoping. With lexical scoping, the run-time must incorporate some mechanism to find the stack frame of a lexical parent (as seen in the program's source code) to access a nonlocal variable's value. In dynamic scoping the run-time can just follow the stack frame order (starting at the top) to find a nonlocal variable's binding.
Early LISP used dynamic scope. Scheme had lexical scope from the beginning. Common Lisp had both mechanisms and programs can use both.
The implementation of recursion also has to address proper access to nonlocal variables in functions that are values themselves and are passed as arguments to other functions. Do these functions access the nonlocal variables based on their call location or their lexical location in the source code? These problems with functions as arguments are known as the upward and downward funarg problems. Knuth wrote the man-boy program to test Algol 60 implementations in these areas.
Another complication for implementors of Algol 60 was parameter passing by-name, which is neither by-value nor by-reference. I don't recall any other well known language that has subsequently made that non-intuitive (to me) choice. I believe that Algol 68 abandoned call by-name, but it's been 25 years since I looked at the Algol 68 standard.
The closest analog of call by-name I can think of is Common Lisp macros.
If actually evaluating the expression is something expensive and its result might not be needed, it can be the right thing. But whoever designs the function interface has to anticipate that possibility.
But then maybe Alan Kay will show up and clarify.
I'm just old enough to remember when corporate culture was like this too. It used to be OK to say when people were wrong or get mad when programming errors lit the building on fire. That started to become NOT OK in the past 15 years. A lot of older engineers really had to to work hard to adapt because it's so frustrating today when people make careless mistakes over and over again and no one can say a word without being accused of not being a team player or something.
People were more likely to admit their own mistakes then too. In that environment it was better to come clean then try to hide a mistake even when coming forward can solve the problem faster.
We've overcorrected this stuff.. correcting it helps make the field more inclusive but at some point after we're diverse and inclusive we need to walk some of this behavior back a bit.
A good quote from Dave Evans (to faculty members who complained about a genius faculty member who could be abrasive): "We don't care if they're prima donnas as long as they can sing".
As I've mentioned in a few other places, including this forum, most people found Edsger to be funny. He obviously enjoyed wielding English for comments, biting, snide, and otherwise. He loved to project snide arrogance in his particular highly developed style.
A good friend of his was Bob Barton -- I think even more of a genius -- and perhaps even more idiosyncratic, pointed and neurotic. Barton was kind of on-stage most of the time, and had truly eloquent extemporaneous opinions.
But so what? Listen to Dave Evans, and then listen to what great and interesting people have to say.
One of the definitions for these people is that whether they are right or wrong, or whether you agree with them or not, what they say is so interesting that it absolutely demands to be thought about.
You can't beat that kind of help for your own thinking processes.
That's the archive, talked about in the linked article. Letters (mostly) that he wrote and sent out to people. Today we'd consider their content and length equivalent to a technical blog. Some were much longer, though.
I have always wondered why his approach of constructing correctness proof along with the implementation never really caught on. I think it was what allowed him to come up with his novel algorithms. Have we lost something of the real essence of logical thinking here? Perhaps the paper mentioned in the article; Social Processes and Proofs of Theorems and Programs which he was vehemently against, will give me the other side of the argument.
People assume this is true because it has been repeated endlessly. I think it is an issue of granularity. For example; both Dijkstra's GCL and Hoare's Triples (fine granularity) vs. Meyer's DbC (coarse granularity) can be expressed using Assertions to build Preconditions/Postconditions/Invariants as "correctness proof" throughout a real-world software system. But their systematic usage is never taught nor enforced; we have to learn it by trial and error.
> For example; both Dijkstra's GCL and Hoare's Triples (fine granularity) vs. Meyer's DbC (coarse granularity) can be expressed using Assertions to build Preconditions/Postconditions/Invariants as "correctness proof" throughout a real-world software system
The average dev at an average company will read this and not understand 90% of your sentence. Again, the vast majority of devs are not computer scientists nor mathematicians.
They are good at what they do, which is building what their bosses ask for using whatever web framework they specialize in.
An organisation that treats its programmers as morons will soon have programmers that are willing and able to act like morons only. -- Bjarne Stroustrup
We all were "average programmers" at one time and didn't know better. But at some point some of us came to know(from whatever source) of a "better and correct way" of doing things and then realized that this should have been taught from the beginning. It is not enough to just teach people the syntax of a language and let them loose on the World; we have to be taught "discipline" and how to use it "correctly". In the context of this thread, that was exactly what Dijkstra strongly advocated for (see my other reply to you listing some paragraphs from EWD288).
References (Wikipedia is a good starting point though sometimes overly complicates simple ideas):
* Dijkstra's GCL - https://en.wikipedia.org/wiki/Guarded_Command_Language
* Hoare's Triples - https://en.wikipedia.org/wiki/Hoare_logic
* Meyer's DbC - https://en.wikipedia.org/wiki/Design_by_contract
* Assertions/Preconditions/Postconditions/Invariants - https://en.wikipedia.org/wiki/Assertion_(software_developmen... - https://en.wikipedia.org/wiki/Precondition - https://en.wikipedia.org/wiki/Postcondition - https://en.wikipedia.org/wiki/Invariant_(mathematics)#Invari...
My thesis is, that a helpful programming methodology should be closely tied to correctness concerns. I am perfectly willing to admit that I myself may be the most complete victim of my own propaganda, but that will not prevent me from preaching my gospel, which is as follows. When correctness concerns come as an afterthought and correctness proofs have to be given once the program is already completed, the programmer can indeed expect severe troubles. If, however, he adheres to the discipline to produce the correctness proofs as he programs along, he will produce program and proof with less effort than programming alone would have taken.
The framework of this contribution does not allow the inclusion of a worked-out example. Instead I shall try to sketch how the hand-in-hand construction of a program and its correctness proof guides the programming process.
I found what I regard as the quintessence of this methodology in the summer of 1968, when my attitude towards flowcharts changed radically. Up till that moment, I had regarded a flowchart as something incomplete, as a plan, as a (half-pictorial, but that is not essential) representation of my intentions, something that as a description would only make sense if all further details, down to the bottom, had indeed been supplied. But it was then that I saw that such a sketch of a program still to be made, could be regarded as an abstract version of the final program, or even, that it could be regarded as "the program", be it for a —in all probability hypothetical— machine with the proper repertoire of primitive actions operating on variables of the proper types. If such a machine were available, the "rough sketch" would solve the problem; usually it is not available, and actions and data types assumed have to be further detailed in the next levels of refinement. It is the function of these next levels to build the machine that has been assumed to be available at the top level, i.e. at the highest level of abstraction. This most abstract version is now no longer a draft of the final program, it is an essential part of the total program; its correctness is independent of the lower level refinements and can be established beforehand. To give this correctness proof before proceding with the lower level refinements serves many purposes. It establishes the correctness of the top level. Fine, but what is more important is that we do this by applying well-established theorems applicable to well-known sequencing clauses, and as a result it becomes most natural to avoid clever constructions like the plague. But the most important consequence is that the proof for one level ensures that the interface between itself and the lower levels has been given completely, as far as is relevant for that level; and also, by fixing in the interface only what the correctness proof really needs, the interface can be kept free from overspecification.
Finally, a word or two about a wide-spread superstition, viz. that correctness proofs can only be given if you know exactly what your program has to do, that in real life it is often not completely known what the program has to do and that, therefore, in real life correctness proofs are impractical. The fallacy in this argument is to be found in the confusion between "exact" and "complete": although the program requirements may still be "incomplete", a certain number of broad characteristics will be "exactly" known. The abstract program can see to it that these broad specifications are exactly met, while more detailed aspects of the problem specification are catered for in the lower levels. In the step-wise approach it is suggested that even in the case of a well-defined task, certain aspects of the given problem statement are ignored at the beginning. This means that the programmer does not regard the given task as an isolated thing to be done, but is invited to view the task as a member of a whole family; he is invited to make the suitable generalizations of the given problem statement. By successively adding more detail in the lower levels he eventually pins his program down to a solution for the given problem.
Sometimes these interview stories sound like selecting a professor of mathematics by picking the one who can calculate the square-root-of-2 to 12 digits in their head the fastest.
When I watched it I was both studying Computer Science and learning Dutch, so it was twice as interesting. The version I linked provides English subtitles.
Most of the good work on escape analysis started around ~2010
Rust got us rolling on borrow semantics (I have a feeling the '20s will be remembered as the the golden age)
I'm sure there's a thing or two in or around LLVM that would rank, but I'm not paying close enough attention.
From a 'renaissance' standpoint:
- LZ-family compression algorithms
- Multi-tenant process isolation (containers)
- transport protocols
- Consensus algorithms
Speaking of which, there's been great progress in low-pause garbage collection over the last few years, although it could be said that Azul was doing it a while back.
Many of those 90's GC algorithms complained of a lack of a cheap instruction for write barriers, and some were specifically about amortizing write barriers by using coarser grained ones. Azul's pivot to software only solutions came on the shoulders of Intel's VT instruction set, which allows, among other things, for nesting of virtual memory. The Azul JVM essentially behaves as a VM.
[ETA] and some of the other GCs now leverage the vast open space of 64 bit addressing to alias memory addresses to give references 2 or 3 flavors, and use that to coordinate parallel GC activities.
Zip was an ahead-of-time compression algorithm until HTTP 1.1, and so the draw was storage and transmission bandwidth, but the deciding factor was decompression time and space complexity.
Now we've been using it for online compression so long, and bandwidth is a secondary concern. Eventually someone had to take the other constraints seriously. We made LZO and friends but the results weren't that exciting, and I think a lot of people wandered off for another 10 years to work on other things, until bandwidth became a bigger concern for producers than consumers.
For containers, I'd love to talk to some mainframe OS designers about how much of containers and The Cloud are merely democratizing techniques that were proven out on big iron 30 years ago. I suspect the answer is "a lot".
1. classification (Andrew Ng @ YouTube): https://www.wired.com/2012/06/google-x-neural-network/
2. Language Translations (NLP, word2vec): https://www.technologyreview.com/2020/10/19/1010678/facebook....
3. Transfer learning
4. SnapChat's Face Filters and real time ML for AR: https://screenrant.com/snapchat-anime-face-filter-lens-effec...
5. Apple iPhone's neural engine and Face ID
(He loaned me a copy of a book on Frege's logic during the course---it had been signed and given to him by the person who let him stay on their floor when he first came to the US.)
The link brings to a paywall. FFS do they really have the courage to ask 42,64€ for a paper from 1960 ?
MR33, Mathematisch Centrum, Amsterdam, 1960. https://ir.cwi.nl/pub/9253
Or maybe he even was able to comment on it, I am not sure how far the field had moved while he was still with us. I have searched for it but could find any comment from him on the subject.
Actually, based on the above I think he would have been all for it.
Well, I mean knowing Dijkstra he would have found something to complain about :D, but it wouldn't have been that it wasn't imperative enough!
Was this article written by Dijkstra himself?
There will always be someone in every Hacker News comment section to whine like a baby. Every topic, every thread. Someone will whine.
To gain context into Dijkstra's response, it may be worth reading it [0]. Here's the conclusion of his response:
> In short, the article is a progress report on a valid research effort but suffers badly from aggressive overselling of its significance, long before convincing results have been reached. This is the more regrettable as it has been published by way of Turing Award Lecture.
Regarding "He tried to destroy it." Dijkstra is known, and often criticized by others, for his hyperbole. Perhaps instead of imitating this heavily criticized aspect of his, you could tone down your rhetoric and actually create an argument rather than try to dismiss someone (and all their work) for one thing you disagree with.
[0] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD06xx/E...
Regardless, your original comment made two absurd claims:
1. Dijkstra attacked the paper that inspired Haskell and everything else that currently exists in FP. He tried to destroy it. [emphasis added]
Which is what my quote of Dijkstra's actual statements was meant to rebut. He did not try to destroy it. He criticized it, and some of his criticism may have been wrong then, and I'd say is wrong now (with greater understanding of the ideas Backus was presenting), but he did not try to destroy it.
2. He should be a footnote in history.
Another absurd position. Because of one response (and if you wanted to you can probably find a number of others) exaggerated beyond reason ("He tried to destroy it."), you want to dismiss some 50 years of work.
"He tried to destroy it" is too strong. I will back down from that.
And I 100% agree. Thinking that functional programming solves all problems is a fundamental misunderstanding of computation.
The first thing that opened my eyes to the overselling of FP as a panacea was reading Leslie Lamport’s work, specifically Computation and State Machines: https://lamport.azurewebsites.net/pubs/state-machine.pdf. Specifically, in Section 3: Programs as State Machines, he demonstrates how the same algorithm for computing factorials can be implemented via mutation or recursion.
With TLA+, Lamport also showed that mutation and state can be reasoned about mathematically, contrary to the central claim of functional programming purists.
The point is simple: functional programming doesn’t in any way _inherently_ help with correctly implementing programs. The fact that FP is currently in vogue is simply another example of how humans don’t require any evidence of anything at all before following a belief system blindly.
FP does prevent certain classes of mistakes from happening, i.e. unintentional bugs due to mutation creating implicit state machines. But preventing bugs and aiding in correctness aren’t exactly the same thing.
While Dijkstra's criticism probably does deserve to be called an "attack", the resulting exchange between him and Backus was highly thought-provoking and entertaining.
https://github.com/jiahao/backus-dijkstra-letters-1979/
https://medium.com/@acidflask/this-guys-arrogance-takes-your...
> He should be a footnote in history.
Please read the posted article, and educate yourself on his historical significance.
https://en.wikipedia.org/wiki/Edsger_W._Dijkstra#Pioneering_...
Not that I don't wish it were otherwise. I love the beauty of mathematics and do wish software were more elegant.
I think he is actually underrated. I'd have liked to be introduced to his proof notations during some formal courses on my CS formation, which was never mentioned.
Think of Dijkstra as Sherlock Holmes thought of himself; viz.
My dear Watson,” said he, “I cannot agree with those who rank modesty among the virtues. To the logician all things should be seen exactly as they are, and to underestimate one’s self is as much a departure from truth as to exaggerate one’s own powers.
But you see the same with Linus Thorvalds. His tone offends a lot of people in particular Americans.
But as a fellow Nordic I think the passive aggressiveness often observed in America or fake politeness more difficult to deal with.
Of course Dijkstra and Linus are quite different personalities but both suffer from an English speaking majority thinking their concepts of proper etiquette is universal.
This reminds me one thing I find irritating about SF in general and SF movies in particular. They hardly portrait technology use in an organic way. Do you want to see a great SF movie? Watch a current normal movie with 1990s eyes. People will text, call her friends, use Uber, buy on Amazon but nothing self conscious " See? See how cool is what I am doing!?"
That's a good example. I often do the reverse: watching 90s or older movies with modern eyes. It can be incredibly refreshing to watch older movies that have a slower and more relatable vibe.
The Norse God spirit of Linus Torvalds.