Lamport and how Education works: The Coming Software Apocalypse
October 30, 2017 at 7:00 am 20 comments
Several people sent this article to me. It’s so one-sided and contrary to empirical evidence that I found it hard to finish. The belief that we can fix all of software through the use of software proofs and verification is contrary to software social processes, as shown by DeMillo, Lipton, and Perlis in 1979. Belief that Toyota sudden acceleration was due to a software bug ignores the empirical evidence about other causes for the phenomenon (as Gladwell described in his podcast last year).
It’s the paragraph quoted below that led to people sending me the article. Leslie Lamport suggests that if we just taught people TLA+, that would lead to better software.
Education of novices never works as a mechanism to change professional practice. (Or at least, I’ve been trying to find an example of successfully changing a community through education of the young, and I haven’t found one yet.) Students who want to become software developers want to do what software developers do — that’s Lave and Wenger’s model of situated learning, where students join a Community of Practice through Legitimate Peripheral Participation (which I describe in this blog post). If you tell students to learn TLA+, you would most likely get a response like, “Why are we learning THIS? We want to real thing, not some academic toy!”
If you want to change a community of practice, you have to get the leaders in the community of practice to change. Students follow them. It doesn’t work the other way around.
But TLA+ occupies just a small, far corner of the mainstream, if it can be said to take up any space there at all. Even to a seasoned engineer like Newcombe, the language read at first as bizarre and esoteric—a zoo of symbols. For Lamport, this is a failure of education. Though programming was born in mathematics, it has since largely been divorced from it. Most programmers aren’t very fluent in the kind of math—logic and set theory, mostly—that you need to work with TLA+. “Very few programmers—and including very few teachers of programming—understand the very basic concepts and how they’re applied in practice. And they seem to think that all they need is code,” Lamport says. “The idea that there’s some higher level than the code in which you need to be able to think precisely, and that mathematics actually allows you to think precisely about it, is just completely foreign. Because they never learned it.”
Source: The Coming Software Apocalypse – The Atlantic
Entry filed under: Uncategorized. Tags: LPP, situated learning, undergraduate.
Computing Ed Research - Guzdial's Take 
1.
Neil Brown | October 30, 2017 at 7:45 am
I suggest a slight clarification: when you say “Education never works as a mechanism to change professional practice” I’m guessing you mean “education of novices”/”university education”? Educating the community leaders presumably could work.
2.
Mark Guzdial | October 30, 2017 at 7:47 am
Thanks, Neil. I’ve updated the post — yes, I meant education of novices.
3.
Mark Guzdial | October 30, 2017 at 10:26 am
Based on the email messages I’m receiving, I did not make my points clear to those developing formal methods tools. I’ll try to explain better here.
My post is about social issues, not technical ones. I read the DeMillo, Lipton, & Perlis article as saying that we do not have the social infrastructure in software engineering to prove programs correct. Mathematics cares about correctness and spends a lot of effort on proofs. Software engineering today is oriented towards meeting requirements, not proving correctness. There is too little labor in software engineering today to meet requirements. There is simply not enough labor available in software engineering to also prove correctness. Given that the article about “The Coming Software Apocalypse” was written this year (i.e., formal methods and proofs about software are still uncommon), it seems like the 1979 argument is still valid.
To show that you can change professional practice through education of novices, you need to show three things:
I would love to find an example of this working. Anyone have one? In 2016, doctors still didn’t wash their hands, so I’m still looking for an example.
4.
Taylor Johnson | October 31, 2017 at 10:55 am
Thanks for the post! I’d like to make a few points as someone in formal methods and model-based design.
First, I didn’t get the argument from the article that teaching students representative examples of formal methods such as TLA+ would result in more reliable software/systems. My perception of what’s being argued in the article is that educating students with a more solid mathematics background, as well as focusing on higher-level architecture and design in practice, such as through model-based design, may help.
“For Lamport, a major reason today’s software is so full of bugs is that programmers jump straight into writing code.”
“Though programming was born in mathematics, it has since largely been divorced from it. Most programmers aren’t very fluent in the kind of math—logic and set theory, mostly—that you need to work with TLA+.”
I don’t think anyone in formal methods thinks they are a panacea to fix all issues in software, nor that educating the masses would necessarily accomplish much. It’s not in any undergraduate curriculum as far as I’m aware (beyond maybe automata theory in a theory of computation class), and at least I didn’t see formal methods until grad school. I would agree that many improvements that can be made are in terms of the design process and social elements, not in technical solutions such as an all-powerful formal methods tool.
I think most folks in formal methods would argue that the simple act of formalization of specifications/requirements and possibly of algorithms/models provides the biggest benefit of their usage, not in actually proving correctness. This benefit can help identify inconsistencies in requirements and make the higher-level abstraction and architecture clearer, so that bugs/issues are found early before building the system/programming begins. Due to NDAs, I cannot state details/numbers, but this has helped in a large way (in terms of development and verification/validation cost) for practical systems such as cars and aircraft.
Second, I listened to some of the Gladwell podcast. While I agree there are a combination of factors in the Toyota unintended acceleration, such as psychological factors causing drivers to push the accelerator instead of the brakes and floor mats sticking, the Bookout case expert testimony found software task death issues that could cause brake assist to fail. Without brake assist, it’s nearly impossible to stop a vehicle with a fully open accelerator, and perhaps this task death led to black box data being missing regarding brake status. A great overview is here:
https://betterembsw.blogspot.com/2014/09/a-case-study-of-toyota-unintended.html
Click to access koopman14_toyota_ua_slides.pdf
Third, while formal methods education is unlikely to happen at a large scale in practice, there are some other recent empirical results illustrating its benefits and issues to address.
1) The DARPA HCAMS project (https://www.darpa.mil/program/high-assurance-cyber-military-systems) built the most secure drone in existence (http://ssrg.nicta.com.au/projects/TS/SMACCM/) as evaluated through red teaming using formal methods and the seL4 formally verified microkernel (http://ssrg.nicta.com.au/projects/seL4/).
2) DARPA estimates there are ~1000 formal methods experts in the US. This is a workforce development and educational issue that could be addressed.
Click to access hacms-stanford-apr_2015.pdf
3) Other recent results such as the formally verified optimizing C compiler CompCert (http://compcert.inria.fr), for which fuzzing bug finding approaches such as CSmith (https://embed.cs.utah.edu/csmith/) found hundreds of bugs in GCC and LLVM, did not find any in the formally verified parts of CompCert (http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf).
Now, both seL4 and CompCert are huge undertakings that did rely on the use of automated/interactive theorem provers (Isabelle and Coq respectively) for establishing higher-order logic specifications. It’s unlikely that the use of such theorem provers, of which TLA+ is another example, will become mainstream, and theorem provers are somewhat fringe approaches even in formal methods today.
4) Most modern microprocessors are designed using formal methods, mostly automated ones, such as model checking, equivalence checking, test-case generation, etc. in a now commoditized segment of the EDA market (http://www.cs.utexas.edu/users/moore/acl2/seminar/2011.09-22-slobodova/MEMOCODE2011.pdf) provided in part by vendors such as Cadence (https://www.cadence.com/content/cadence-www/global/en_US/home/tools/system-design-and-verification.html), Mentor Graphics (https://www.mentor.com/products/fv/questa-property-checking), and Synopsys (https://www.synopsys.com/verification/static-and-formal-verification.html). The status for software verification is not there yet due to many issues regarding semantics, state-space explosion, requirements formalization, etc., although usage and investments are being made in industry and academia, such as the article’s summary of Amazon’s AWS usage (http://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf), Microsoft’s usage (https://www.microsoft.com/en-us/research/group/research-in-software-engineering-rise/) with test-case generation and driver checking, NASA’s broad usage (https://shemesh.larc.nasa.gov/NFM/ and https://shemesh.larc.nasa.gov/fm/) with SPIN ( http://spinroot.com/gerard/ ) and PVS (https://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/), Frama-C (http://frama-c.com/), Airbus ( http://projects.laas.fr/IFSE/FMF/J1/P04_JSouyris.pdf ), Facebook (https://research.fb.com/publications/moving-fast-with-software-verification/), etc.
5) Finally, modern formal methods focuses exactly on the correctness problem you’ve stated (“Software engineering today is oriented towards meeting requirements, not proving correctness.”), i.e., that is the definition of correctness, as a system/program cannot be “correct” without saying what correctness means, which is done through requirements.
To ensure software/systems meet their requirements/specifications/properties. To establish this mathematically requires (a) a formal specification of the requirements, (b) a model of the system/software, and (c) typically an automated or semi-automated method for checking if the model satisfies the specification, which is typically a model checker, although could be a theorem prover. Of course, in practice the verification and validation process attempts to ensure requirements informally (e.g., test until money/time is run out), but what I got from the article and the status of formal methods, this may not be enough.
Hope these pointers are useful!
5.
Mark Guzdial | October 31, 2017 at 12:42 pm
Taylor, you make a strong argument for formal methods. Evidence doesn’t convince anyone, unfortunately. This has been a theme in this blog before. We have evidence-based methods for teaching CS, and we can’t convince faculty to use them. Authority (people in the center of the community of practice) is more likely to convince practitioners (software engineers or faculty) than evidence. https://computinged.wordpress.com/2015/07/15/the-11th-top-myth-of-teaching-computer-science/
6.
pressron | November 1, 2017 at 4:41 am
Excellent response, just a minor correction: TLA+ is not exactly a theorem prover like Isabelle or Coq. It is a specification language that _has_ a theorem prover which one can use to verify specifications, but it also has other tools, like a model-checker, that can automatically check specifications (or you can choose just to specify and not verify at all). In addition, TLA+ is very flexible in choosing the level of detail, and accordingly, the specification/verification effort required. This (and the fact that TLA+ is a much simpler language than Coq or Isabelle) makes the cost of both learning and using it orders of magnitude smaller, which is precisely why Amazon (and other companies) can use it on an industrial scale. AFAIK, Amazon only verifies specifications using the model-checker, not the proof assistant, and they do not perform end-to-end verification (i.e., verifying that global correctness properties are preserved all the way down to source- or machine-code level), but rather specify and verify at the abstraction level they find most important. They do not expend anywhere near the amount of effort required for CompCert or seL4, despite their software being one or two orders of magnitude larger.
7.
Alan Fekete | November 1, 2017 at 11:27 am
Taylor said “It’s not in any undergraduate curriculum as far as I’m aware (beyond maybe automata theory in a theory of computation class)” This comment seems to me to reflect Taylor’s limited variety of experiences but not the facts about university curricula (maybe he has focused only on universities in the USA, rather than internationally).
Formal methods have been taught extensively in undergraduate education in other countries for decades now. In Australia, the Software Engineering degree at University of New South Wales included major second-year projects using B Method and its tooling (I understand this content was dropped a few years ago, when Ken Robinson, who was the enthusiast behind it, retired). UQueensland was similarly teaching formal methods, with a major research group in the area (Ian Hayes, David Carrington, etc) having a lot of influence on their curriculum. For a long time, Z was part of the first or second year education of undergraduates studying CS at many universities in UK, like Oxford, Cambridge, Imperial College, Edinburgh etc etc.
[I do find it distressing how often discussions in the USA forget the existence of other, very different, educational systems]
8.
Taylor Johnson | November 1, 2017 at 11:55 am
Thanks for the comment Alan and pointing out the differences in international curricula. Yes, I meant this as any US-based undergraduate curriculum and did not intend for the statement to apply internationally. The comment I made of DARPA estimating ~1000 formal methods experts in the US is indicative of the better status of formal methods education internationally, as well as programs such as DARPA’s HACMS supporting researchers in Europe and Australia, in addition to the US.
9.
Alfred Thompson | October 31, 2017 at 12:20 pm
The idea seems to be that novices will enter industry and tell people with 5 to 20 years of experience that they are doing it all wrong and those experienced people will drop what they have been doing a listen to the newbies. Never happen. My experience is that new graduates are told to forget what they learned in university and do it the way the rest of the team does it. It takes years before people get to push their own ideas on others. By that time most are assimilated.
Ideas in the companies I have worked at over the years are pushed top down not bottom up. Convincing the experienced people to change, which is hard, is the only way industry changes.
BTW The idea that professors who generally do not change how they teach based on research expect industry to change the way they develop software based on research is somewhat amusing to me.
10.
shriramkrishnamurthi | October 31, 2017 at 11:07 pm
Except, of course, for the counter-examples: the adoption of compilers, of garbage collection, of type-safety, of scripting languages… Other than the exceptions, your theory is watertight. (-:
11.
Alan Fekete | November 1, 2017 at 11:19 pm
I am not sure whether the claim is that these are counter-examples to Mark’s view, that one can’t change industry by teaching undergraduates a new practice, or counter-examples to Alfred’s stronger view that industry changes come top-down rather than bottom-up. If they are offered against Alfred’s view, then I don’t have anything to offer on the issue; but if they are raised to counter the claim that ideas can’t be spread from the university classroom, then I suggest that some at least of these are not valid counter-examples.
As far as I know, compiled languages (eg Fortran, COBOL) spread in industry even before computer science was an academic discipline in most campuses.
Would you agree that the first language with garbage collection that was widespread in industry was Java? My recollection is that Java was spreading in industry concurrently with its spread in universities as a first teaching language (when it was all the rage in both industry and academia, as the way to program the Internet!).
I believe that scripting languages were popular in industry for building dymanic websites (PHP, Perl etc) long before they were widely taught in universities. Python is now becoming very popular in teaching intro CS, but industry was there first.
What would you classify as the first (reasonably, though not perfectly) typesafe language in widespread industry use? Would you count Pascal or C? If so, that may be a counter-example, as I claimed these in another comment here.
There are certainly lots of examples of industry trends that came from university research, but that doesn’t mean they spread because of the research, let alone because of teaching. One recent example is Spark; this was invented in Berkeley’s AMPLab, and I understand that it spread to industry because the grad students behind it (esp Matei Zaharia) were so active in talking about it at meetups etc, and made it available open-source with lots of support from the inventors. I don’t think the technology was getting taught anywhere except a few Berkeley (upper-level, elective) classes.
12.
shriramkrishnamurthi | October 31, 2017 at 10:26 pm
The fact that Mark keeps talking about “correctness” implies that he does not understand anything about modern formal methods, and by “modern” I mean “since 1979”. It’s a pity that instead of trying to understand it better, such as trying to really _understand_ Taylor Johnson’s excellent and detailed response, he dismisses of it with (his equivalent of) snark.
I was tempted to say nothing — sometimes a message and the author’s follow-up remarks are so off base that it seems pointless — but given Mark’s authority and following, that would be dangerous in giving later readers the impression that Mark is as much in the know as his authoritative words suggest. So I’ll just say, if you want to understand these issues better, get in touch with me or someone else who actually does (and understands) formal methods.
13.
Mark Guzdial | November 1, 2017 at 11:49 am
I don’t know or understand modern formal methods — guilty as charged. My argument isn’t about formal methods, though. By referencing the DeMillo, Lipton, & Perlis paper, I probably set off all kinds of alarm bells that I was against formal methods, when that wasn’t my point at all. I was disappointed that “The Coming Software Apocalypse” didn’t consider social considerations, like those raised in the 1979 article, and that’s why I mentioned it.
My main argument is with Lamport’s point, that the reason why tools like TLA+ haven’t been adopted widely is because of “a failure of education.” I’ll quote again the most relevant three sentences.
Set aside formal methods or verification or specification. The idea that we can change industry by changing how we educate future practitioners is not supported by education theory or empirical findings. That’s my point. Alan thinks that UNIX, Pascal, and C made it into industry through classrooms, and that would be a counter-example to my claim. I’d love to find evidence that that’s true, and if true, I’d like to understand how that happened since it’s counter to LPP and situated learning theory.
I do appreciate Taylor’s detailed response — it’s fascinating! Perhaps I missed something in one of the links, but it seemed to me like he was showing evidence that formal methods are powerful and useful. I buy that. That doesn’t contradict my argument that industry adoption does not occur through classrooms. I offered an analogy. Attempts to get teachers to change their practices are rarely furthered by evidence. Most times, change in education practice comes from top-down leadership and authority. I’ve been digging into some of this literature lately, and there is certainly evidence to suggest that change in higher ed teaching usually comes from a Dean or Chair or Dept Head deciding to make it an issue. I’m offering that to Taylor as a possible way that change might happen in software engineering practice. No snark intended.
I see Alfred as backing that point. In his experience, change in software development practices have always occurred top-down, not driven by the latest hires. You suggest that “the adoption of compilers, of garbage collection, of type-safety, of scripting languages” are counter-examples. Were those innovatives all achieved through education practice, not through leadership and authority? I’d love to read studies of the adoption of those innovations, if you could point me to any, please.
I should put a caveat on my first paragraph. I am interested in the work regarding software engineering for end-user programming, which includes verification and specification systems for tools like spreadsheets. I’ve read at least one paper by you in that area. Do you consider those formal methods? If so, then I do have to amend my earlier statement — I know something about modern formal methods. My argument is still not about them.
14.
Taylor Johnson | November 2, 2017 at 11:50 pm
Thanks Mark! I didn’t take any offense. I was trying to get across two points, specifically in regards to your comment “The idea that we can change industry by changing how we educate future practitioners is not supported by education theory or empirical findings.”
1) I really don’t think Lamport was arguing that teaching formal methods to students would get them to use it in industry. I think he’s arguing that practitioners (a) may not have the requisite background education (specifically math) to be able to use formal methods even if their bosses or other authority figures told them to do so, and (b) that they may not be designing/thinking before writing code, specifically, the development of requirements and specifications may not be sufficient (e.g., blueprints for architects before construction starts). Further, regarding the authority standpoint, I’m not sure how much more authoritative one could get than a Turing laureate saying to use them… 🙂
Here’s a talk by Lamport that further illustrates this viewpoint:
2) The other part of my point was that formal methods are already somewhat widely used in industry (depending upon the industry), and folks in this area already know this. It makes your suggestion that the article is arguing to change how students are educated possibly influencing industry change somewhat moot. Specifically, they are widely used in semiconductor design, and they are increasingly being used in cyber-physical systems (CPS) industries, such as automotive, aerospace, medical devices (https://www.fda.gov/MedicalDevices/ScienceandResearch/ResearchPrograms/ucm477412.htm), train control, nuclear, etc., as all of these are safety-critical.
As another example, most if not all aerospace companies/agencies have formal methods groups, with Airbus and NASA referenced in my earlier comment, but this is true for the others, and the article mentions some of these. In addition to languages amenable to formal verification, such as the article’s discussion of Esterel, there are formal methods integrated within Matlab and Simulink through Polyspace (https://www.mathworks.com/products/polyspace.html) and Simulink Design Verifier (https://www.mathworks.com/products/sldesignverifier.html). From a market standpoint and where formal methods industrial usage is headed, you can imagine why Ansys thought it was a good idea to acquire Esterel a few years ago, and likewise why MathWorks thought it was a good idea to acquire PolySpace.
Related to the Toyota example, you might also look at how Toyota has been investing following the unintended acceleration issues to better understand where the real issues may have been in contrast to Gladwell’s opinion, e.g., Toyota has a formal methods group that got started following it. This is somewhat comparable to the semiconductor industry’s investment into formal methods throughout the 90s following the Pentium FDIV bug that caused Intel to recall Pentiums at a cost at the time of several hundred million dollars, or inflation adjusted around a billion dollars today. In contrast, so far the Toyota issue has cost several billion dollars, see, e.g. section 5.3 in this paper, and this cost is also mentioned in the Atlantic article:
Click to access 24ESV-000063.PDF
As further evidence, here’s a good keynote illustrating this from Toyota, from one of the top CPS formal methods venues (HSCC):
Will future cars have formally verified powertrain control software?
Jyotirmoy V. Deshmukh, Toyota
http://ljk.imag.fr/hscc2015/keynote.html
http://www.cs.utexas.edu/~deshmukh/Papers/Talks/hsccKeynote.pptx
Overall, I’m just trying to get across that formal methods are already used in industry, as I really did not get your interpretation from the article that they’re being suggested to be taught to students so they’d be used by future practitioners. Additionally, enabling a broader usage of them in industry may benefit from having practioners with the requisite math background—presumably learned at least in part while they’re students—to be able to learn how to use them if/when it comes up that they need to do so in their job, either for regulatory reasons (e.g., recent versions of aerospace standards such as DO-178C and DO-333, https://shemesh.larc.nasa.gov/people/bld/ftp/NASA-CR-2014-218244.pdf of which they are comparable variants in other safety-critical industries) or because their boss/other authority figure told them to do so. Finally, I think the article did a good job illustrating how Newcombe convinced his colleagues to try using formal methods, part of which was largely a social issue.
15.
Alan Fekete | November 1, 2017 at 5:15 am
I was only a student in the late 1970s/early 1980s, but I got the sense that the use of Unix and shell (and the composition of tools philosophy that go with them), the use of Pascal (and the use of structured programming techniques that Pascal largely enforces), the use of C, were all ideas that were initially taught in universities to novices at that time, and later these spread to wider industry practice. I certainly remember instructors explaining why these ideas were superior to industry practices like Fortran and IBM operating systems, and worth learning even though industry did it differently.
I always assumed that the mechanism for tech transfer in that time was by university-trained employees, pushing in the workplace for the tools they liked (and the graduates knew these were easier or more productive, compared to what was common in industry at the time). Can someone older, or more knowledgable about the history of computing, clarify whether this case is an example of universities driving industry change?
16.
Mark Guzdial | November 1, 2017 at 8:34 am
Would you accept a friendly amendment to your question, Alan? I think we can find many examples of universities driving industry change, e.g., Berkeley UNIX. Lamport said that it was a “failure of education,” and that’s what I was responding to. I’m arguing that teaching students differently doesn’t drive industry change. The question I’d like to ask is, “Can someone older, or more knowledgable about the history of computing, clarify whether this case is an example of university EDUCATION driving industry change?” Do the newly hired students from the University bring with them the new practices that change how the existing practitioners do things?
17.
Alan Fekete | November 1, 2017 at 11:30 am
Thanks for clarifying my ideas! My belief is that, for Unix, Pascal and C, it was the fact that these were TAUGHT in so many University classes, that preceded (and presumably drove) industry adoption.
18.
Mark Guzdial | November 1, 2017 at 11:31 am
I think that’s a great question. I don’t know.
19.
Bonnie | November 3, 2017 at 7:21 am
I think one thing you guys are all missing is that many developers in industry do not have a computer science background – they are self-taught for the most part. This affects both the technologies being brought in by new hires as well as the ability of veterans to absorb these technologies. Self taught developers are less likely to bring in approaches based on formal methods because it isn’t likely they would have encountered anything like that, and the folks already working in industry without a CS background may not have the background or mindset to absorb formal methods.
When asking questions about whether this or that practice in CS education has an effect on industry, it is important to recognize that so many practitioners in industry never went through a CS program and were never exposed to the practices in question.
20.
Require CS at University in order to Get CS into K-12 (Revisited) | Computing Education Blog | December 15, 2017 at 7:01 am
[…] schools) don’t perceive a need for CS. This is a form of the same problem that came up when we were talking about getting more formal methods into software development practice. All professionals should understand the role of computing in our society and how to use computing […]