13 ms·

The Rise and Fall of Lisp at the Jet Propulsion Lab.

82 points by spydez 18y ago

silentbicycle 18y ago
So it sounds like the JPL's reason (at least the reason they gave - whether you want to believe it was some anti-Lisp conspiracy or just bad office politics is your own business) was that Lisp was too big. I wonder if Scheme would have been a better fit? (It was certainly around in 1988; SICP was written in 1985.) There's something about Lisp that gives it a reputation as inherently individualist (as opposed to the "workers are expendable cogs" project management model that the linked article associates with Java). Same with Forth. At this point, the Lisp community seems to encourage that idea, but what in the language itself supports this? I hear arguments that it's a harder language, but let's not kid ourselves. I think programming well in, say, C++ or Haskell is much, much harder. (Should a language be hard to use well?) Or: Lisp code is hard to read. Potentially, sure -- the readability of the code is more dependent than most languages on the developers' abilities to name things well. (Same with Forth.) You can write unmaintainable garbage in any language, though - just copy and paste things where they're used instead of naming and referencing them, give variables meaningless names, etc. Just add water and presto, big ball of mud. (http://www.laputan.org/mud/ http://www.laputan.org/mud/) Also, most programmers are probably used to good editors handling paren balancing in any language. Besides being significantly different from the main languages people are exposed to, what? All it takes for a language to be different from e.g. C/Java is to not be C/Java. Is it because you can create your own idioms / extensions to the core language? I also think the syntax is something of a red herring - sure, you may dislike the syntax, but I can think of popular languages that have disastrous syntaxes. (I guess Dylan could be a control group here, but I don't know anybody who has real experience with it, let alone its reputation among management.) No answers, but I'd really like to know. Working on my own language, and all that. Also: I'm most definitely not looking for thinly-veiled bragging about how "not everyone can handle such a superior language" either, because... come on.
- jrockway 18y ago
  There's something about Lisp that seems inherently individualist. At this point, the Lisp community seems to encourage that idea, but what in the language itself supports this? I think the people that choose Lisp select it after a study of the various options. Choosing and evaluating programming languages is not a social activity -- you do it by yourself. Contrast this to Java programmers, who use Java because it's what they learned in school. They aren't individualistic, they just do what they are told. (Java's popularity is helped by the "tools" are "easy to use". SLIME and Emacs are "hard to use", so you have to want to use them to be able to use them. I use quotes because I disagree with the sentiment. Eclipse is a nightmare to use. Emacs is a dream.) As for Java's popularity, I think it comes down to social factors rather than differences in the syntax of the language. Java developers want less money than Lisp developers. It's also easier to hire Java developers, because you can just require a Sun certification. Easy!
  - silentbicycle 18y ago
    So you'd say that more Lisp-users tend to be self-taught / come to the language themselves, rather than using $current_job_security_language? This isn't specifically about Lisp vs. Java, though - I don't see people have this sort of kneejerk reaction about Python, for example. (Though Python seems to have been carefully designed to give a first impression of being clean and easy to use. I'd say it mostly is, but it definitely gives a good first impression.)
  - gaius 18y ago
    I don't think that's true. Lisp jobs are few and far between; people who want them really want them. There are many jobs that are like that. Here in the UK nurses and firemen are badly paid, that's because there's always someone who wants the job enough to do it for barely living wages. The only way to be a well-paid Lisp programmer is to work somewhere where they wouldn't even dream of using Java.
    - jrockway 18y ago
      I've found that the better a job suits me, the more they are willing to pay me. (I have never looked for a Lisp job, though.)
- deleted 18y ago
  [deleted]
- gruseom 18y ago
  By "inherently individualist" do you mean that Lisp programmers tend not to work in teams? Or just that there aren't many of them, so they tend to be thinly scattered and thus isolated? My current pet theory is that only a minority of people feel comfortable thinking in s-expressions. For the majority, trees with many levels of nesting aren't a natural medium for expressing their thoughts. (I don't know why this would be, but it's worth pointing out that human language has a very low tolerance for nesting (in fact you almost never see it go beyond level 1)). I know two very good programmers who gave Lisp a good try and just don't feel comfortable in it. So I don't buy the inferiority argument either. Interestingly, both of those guys strongly prefer Smalltalk, which is arguably as close to Lisp-with-all-those-trees-unwound as anyone has got. Edit: I'll add that if the nesting theory is correct, I feel lucky to be in the minority that finds it comfortable to build programs that way... what I'm able to do in Lisp far outstrips what I was able to do before.
  - silentbicycle 18y ago
    I'm trying to figure out what specific characteristics give it the kind of reputation it has. Good observation about Lisp vs. Smalltalk, by the way. (I also wonder why Smalltalk isn't more popular...)
    - gruseom 18y ago
      Ok, here I think you need to look at history rather than the languages themselves. Once Lisp (and Smalltalk, for different reasons) became branded as failures, that reputation was fixed in 90+% of people's minds, and it remains so. This is all the more entrenched because of the bias in favor of the newest things in computing. For most people, that a 40-year old failure might be better than something new and popular just isn't possible.
      - silentbicycle 18y ago
        So, you think it's a legacy of the AI winter?
        18y ago
- DaniFong 18y ago
  Lisp attracts the sort of people who want to bend the language to their will. As such, these same people bend systems, programs, and organizations to their will. Not particularly easy to manage.
  - olavk 18y ago
    bends organizations to their will - if that were the case, Lisp would be used at many more organizations (including Google and JPL), wouldn't it?
    - albertcardona 18y ago
      Precisely it would not be.
    - Darmani 18y ago
      Unfortunately, organizations have a much higher Young's modulus than languages.
      - DaniFong 18y ago
        Unlike languages, they nearly always push back...
- pavelludiq 18y ago
  I personally like scheme, because its beautifully weird. If something is weird, even if beautiful, the type of people that like it are not the best of team players. You don't write poetry in teams. I don't know how much of a team player i am, but from early childhood i got used to doing stuff mostly alone. I guess i could fit well in an extra small team, where one has more autonomy.
  - gaius 18y ago
    The but I'm a poet! attitude partially explains Lisp's unpopularity with large organizations.
    - pavelludiq 18y ago
      Thats strange because i see a lot of job adds requiring creativity and passion. Unfortunately big companies understand creativity as "you should be smart enough to understand your boss's vision" and passion as "You should just do your job and not whine about it".
      - thalur 18y ago
        They also seem to define teamwork as "doing what your boss tells you without pointing out ways to do it better" and leadership as "passing on your boss's vision to the poor souls working for you, while not passing back any complaints/problems to your boss".
    - silentbicycle 18y ago
      Rightly so, I think. Debugging somebody's "poetry" can really suck. I'm not so sure this is necessarily a Lisp thing, though. (And, I'd rather see somebody get creative in code by finding unexpectedly elegant and simple solutions, rather than by adding lots of flourishes.)
- brlewis 18y ago
  No, Scheme would not be a better fit, speaking as someone who codes Scheme day and night. Yes Scheme is smaller, but that's in reality, which makes it totally unrelated to the reasons for rejecting CL.
jimbokun 18y ago
I read this before, but still love this conversation with his Google manager: Me: I'd like to talk to you about something... Him: Let me guess - you want to use Smalltalk. Me: Er, no... Him: Lisp? Me: Right. Him: No way. I just find it an amusing encapsulation of how so many of the high achieving people that Google hires like to program in high productivity languages like Lisp, Smalltalk, Ruby (see Yegge) but Google keeps a tight rein on it by keeping the languages they will deploy on their servers down to 4 or so (Python, C++, Java and Javascript being the 4 I've heard).
- jrockway 18y ago
  It is interesting to imagine what the world would be like if Google had disallowed Java and had written everything in Lisp instead.
  - pchristensen 18y ago
    I do recall Norvig saying that they use C++ for a lot of core code because even though Lisp would be cheaper to develop, they run so many servers that any decrease in efficiency would cost millions (can't find the quote though)
    - jrockway 18y ago
      If making lisp run faster would save someone millions of dollars, lisp would run faster. Sure, it's practical for Google to use C++ in this case [1], but I am imagining a fantasy world. [1] Unless of course bugs that C++ ignores would be caught by Lisp. Perhaps there is a minor type error in Google's code that makes the search results not quite as good. If CL's type checker caught that, they would have gotten super-rich sooner and would own Microsoft right now. But like I said, this is all fantasy. My real argument is "You are not Google."
      - silentbicycle 18y ago
        Making Lisp run faster would almost certainly involve making it closer to SML / OCaml. Beyond algorithmic changes, speed optimization in Lisp usually involves type declarations, or sometimes inference, as in ML. (See: http://www.lrde.epita.fr/~didier/research/verna.06.imecs.pdf http://www.lrde.epita.fr/~didier/research/verna.06.imecs.pdf) Give Lisp a really powerful, inferred static type system and you're most of the way there. (Give it a better module system, while you're at it.) And if you want to talk about a type checker catching bugs... I wish OCaml had kept the s-expression syntax, but it's a very interesting (and powerful) take on improving Lisp. (I think it also helps that they don't call it Lisp. It flies under the radar as far as Lisp's reputation.)
logjam 18y ago
"The situation is particularly ironic because the argument that has been advanced for discarding Lisp in favor of C++ (and now for Java) is that JPL should use "industry best practice." The problem with this argument is twofold: first, we're confusing best practice with standard practice. The two are not the same." To me, this is the crux. We have this ridiculous idea that "industry" drives technological advance. Industry software "engineers" trained up in trade schools or worse, without any awareness that they are reimplementing solutions (poorly) to problems that were solved decades ago...and we get...horrible industrial monstrosities like Java (and Microsoft Windows) roaming the earth, while remote diamonds like Lisp and Scheme shine kindly down.
- silentbicycle 18y ago
  "Come on, dude. You can't argue with best practices. They're the best!" Which is the problem, I think. Their name just screams, "Quit arguing, they know better." (for increasingly nebulous values of 'they'). Aside from trying to undermine the term as a brand ("Best Practices: Because Embracing Mediocrity Looks Good On Paper"), what can you do?
- DaniFong 18y ago
  Java wasn't that crazy. The basic idea of using Java for the web seemed a sane one: the only other alternative was to do something like XWindows. And then what? Are people going to use web browsers like XWindows clients? That would never fly! (oh wait)
- briancooley 18y ago
  Industry software "engineers" trained up in trade schools or worse, without any awareness that they are reimplementing solutions (poorly) to problems that were solved decades ago...and we get...horrible industrial monstrosities like Java Since Guy Steele coauthored both the Lambda Papers (late 1970's) and the first three editions of the Java specification, I don't think that you can successfully argue that awareness of anything solved by Lisp or Scheme was a problem in the development of Java. I always got the impression that the goal with Java was to make bad programmers better, not to create the ultimate language (e.g., see http://fishbowl.pastiche.org/2004/03/17/halfway_between_the_gutter_and_the_stars/ http://fishbowl.pastiche.org/2004/03/17/halfway_between_the_...) To use a golf analogy, consider cavity back irons. The average golfer, who struggles to hit it straight, will likely play a lot better with cavity backs. But a really good golfer won't be able to shape shots easily and will feel hamstrung without his blades.
DaniFong 18y ago
In the words of Elton John: It's sad. So sad. It's a sad, sad situation. My best hope at this point is that the dotcom crash will do to Java what AI winter did to Lisp, and we may eventually emerge from "dotcom winter" into a saner world. But I wouldn't bet on it.
ph0rque 18y ago
> Copyright (c) 2002 So what happened in the ~6 years since then?
- lisper 18y ago
  I quit JPL and started a new career as a VC :-)
  - ced 18y ago
    Do you have that written out in another post somewhere? I loved this one.
    - lisper 18y ago
      Nope. I haven't been doing it long enough to have gotten any good stories out of it yet. I did write this a while back, which was a big hit in its day: http://rondam.blogspot.com/2006/10/top-ten-geek-business-myths.html http://rondam.blogspot.com/2006/10/top-ten-geek-business-myt...
zandorg 18y ago
Lisp at the very least is excellent for initial prototypes.
gibsonf1 18y ago
Is it just me, or is the idea of using a repl on a computer in space simply fascinating?
- bayareaguy 18y ago
  What I found more interesting was this section in the story of the Remote Agent bug ( http://ic.arc.nasa.gov/publications/pdf/2000-0176.pdf http://ic.arc.nasa.gov/publications/pdf/2000-0176.pdf ) One of the errors found with SPIN, a missing critical section around a conditional wait statement, was in fact reintroduced in a different subsystem that was not veriﬁed in this ﬁrst preﬂight effort. This error caused a real deadlock in the RA during ﬂight in space. So the bug fixed with the repl was actually one that was uncovered by the SPIN verifier ( http://spinroot.com/spin/whatispin.html http://spinroot.com/spin/whatispin.html ) months prior to the launch, but wasn't fixed because they didn't verify the code they actually decided to use.

82 points by spydez 18y ago

So it sounds like the JPL's reason (at least the reason they gave - whether you want to believe it was some anti-Lisp conspiracy or just bad office politics is your own business) was that Lisp was too big. I wonder if Scheme would have been a better fit? (It was certainly around in 1988; SICP was written in 1985.) There's something about Lisp that gives it a reputation as inherently individualist (as opposed to the "workers are expendable cogs" project management model that the linked article associates with Java). Same with Forth. At this point, the Lisp community seems to encourage that idea, but what in the language itself supports this? I hear arguments that it's a harder language, but let's not kid ourselves. I think programming well in, say, C++ or Haskell is much, much harder. (Should a language be hard to use well?) Or: Lisp code is hard to read. Potentially, sure -- the readability of the code is more dependent than most languages on the developers' abilities to name things well. (Same with Forth.) You can write unmaintainable garbage in any language, though - just copy and paste things where they're used instead of naming and referencing them, give variables meaningless names, etc. Just add water and presto, big ball of mud. (http://www.laputan.org/mud/ http://www.laputan.org/mud/) Also, most programmers are probably used to good editors handling paren balancing in any language. Besides being significantly different from the main languages people are exposed to, what? All it takes for a language to be different from e.g. C/Java is to not be C/Java. Is it because you can create your own idioms / extensions to the core language? I also think the syntax is something of a red herring - sure, you may dislike the syntax, but I can think of popular languages that have disastrous syntaxes. (I guess Dylan could be a control group here, but I don't know anybody who has real experience with it, let alone its reputation among management.) No answers, but I'd really like to know. Working on my own language, and all that. Also: I'm most definitely not looking for thinly-veiled bragging about how "not everyone can handle such a superior language" either, because... come on.

jrockway 18y ago
There's something about Lisp that seems inherently individualist. At this point, the Lisp community seems to encourage that idea, but what in the language itself supports this? I think the people that choose Lisp select it after a study of the various options. Choosing and evaluating programming languages is not a social activity -- you do it by yourself. Contrast this to Java programmers, who use Java because it's what they learned in school. They aren't individualistic, they just do what they are told. (Java's popularity is helped by the "tools" are "easy to use". SLIME and Emacs are "hard to use", so you have to want to use them to be able to use them. I use quotes because I disagree with the sentiment. Eclipse is a nightmare to use. Emacs is a dream.) As for Java's popularity, I think it comes down to social factors rather than differences in the syntax of the language. Java developers want less money than Lisp developers. It's also easier to hire Java developers, because you can just require a Sun certification. Easy!
- silentbicycle 18y ago
  So you'd say that more Lisp-users tend to be self-taught / come to the language themselves, rather than using $current_job_security_language? This isn't specifically about Lisp vs. Java, though - I don't see people have this sort of kneejerk reaction about Python, for example. (Though Python seems to have been carefully designed to give a first impression of being clean and easy to use. I'd say it mostly is, but it definitely gives a good first impression.)
- gaius 18y ago
  I don't think that's true. Lisp jobs are few and far between; people who want them really want them. There are many jobs that are like that. Here in the UK nurses and firemen are badly paid, that's because there's always someone who wants the job enough to do it for barely living wages. The only way to be a well-paid Lisp programmer is to work somewhere where they wouldn't even dream of using Java.
  - jrockway 18y ago
    I've found that the better a job suits me, the more they are willing to pay me. (I have never looked for a Lisp job, though.)
deleted 18y ago
[deleted]
gruseom 18y ago
By "inherently individualist" do you mean that Lisp programmers tend not to work in teams? Or just that there aren't many of them, so they tend to be thinly scattered and thus isolated? My current pet theory is that only a minority of people feel comfortable thinking in s-expressions. For the majority, trees with many levels of nesting aren't a natural medium for expressing their thoughts. (I don't know why this would be, but it's worth pointing out that human language has a very low tolerance for nesting (in fact you almost never see it go beyond level 1)). I know two very good programmers who gave Lisp a good try and just don't feel comfortable in it. So I don't buy the inferiority argument either. Interestingly, both of those guys strongly prefer Smalltalk, which is arguably as close to Lisp-with-all-those-trees-unwound as anyone has got. Edit: I'll add that if the nesting theory is correct, I feel lucky to be in the minority that finds it comfortable to build programs that way... what I'm able to do in Lisp far outstrips what I was able to do before.
- silentbicycle 18y ago
  I'm trying to figure out what specific characteristics give it the kind of reputation it has. Good observation about Lisp vs. Smalltalk, by the way. (I also wonder why Smalltalk isn't more popular...)
  - gruseom 18y ago
    Ok, here I think you need to look at history rather than the languages themselves. Once Lisp (and Smalltalk, for different reasons) became branded as failures, that reputation was fixed in 90+% of people's minds, and it remains so. This is all the more entrenched because of the bias in favor of the newest things in computing. For most people, that a 40-year old failure might be better than something new and popular just isn't possible.
    - silentbicycle 18y ago
      So, you think it's a legacy of the AI winter?
      - 18y ago
DaniFong 18y ago
Lisp attracts the sort of people who want to bend the language to their will. As such, these same people bend systems, programs, and organizations to their will. Not particularly easy to manage.
- olavk 18y ago
  bends organizations to their will - if that were the case, Lisp would be used at many more organizations (including Google and JPL), wouldn't it?
  - albertcardona 18y ago
    Precisely it would not be.
  - Darmani 18y ago
    Unfortunately, organizations have a much higher Young's modulus than languages.
    - DaniFong 18y ago
      Unlike languages, they nearly always push back...
pavelludiq 18y ago
I personally like scheme, because its beautifully weird. If something is weird, even if beautiful, the type of people that like it are not the best of team players. You don't write poetry in teams. I don't know how much of a team player i am, but from early childhood i got used to doing stuff mostly alone. I guess i could fit well in an extra small team, where one has more autonomy.
- gaius 18y ago
  The but I'm a poet! attitude partially explains Lisp's unpopularity with large organizations.
  - pavelludiq 18y ago
    Thats strange because i see a lot of job adds requiring creativity and passion. Unfortunately big companies understand creativity as "you should be smart enough to understand your boss's vision" and passion as "You should just do your job and not whine about it".
    - thalur 18y ago
      They also seem to define teamwork as "doing what your boss tells you without pointing out ways to do it better" and leadership as "passing on your boss's vision to the poor souls working for you, while not passing back any complaints/problems to your boss".
  - silentbicycle 18y ago
    Rightly so, I think. Debugging somebody's "poetry" can really suck. I'm not so sure this is necessarily a Lisp thing, though. (And, I'd rather see somebody get creative in code by finding unexpectedly elegant and simple solutions, rather than by adding lots of flourishes.)
brlewis 18y ago
No, Scheme would not be a better fit, speaking as someone who codes Scheme day and night. Yes Scheme is smaller, but that's in reality, which makes it totally unrelated to the reasons for rejecting CL.

jimbokun 18y ago

I read this before, but still love this conversation with his Google manager: Me: I'd like to talk to you about something... Him: Let me guess - you want to use Smalltalk. Me: Er, no... Him: Lisp? Me: Right. Him: No way. I just find it an amusing encapsulation of how so many of the high achieving people that Google hires like to program in high productivity languages like Lisp, Smalltalk, Ruby (see Yegge) but Google keeps a tight rein on it by keeping the languages they will deploy on their servers down to 4 or so (Python, C++, Java and Javascript being the 4 I've heard).

jrockway 18y ago
It is interesting to imagine what the world would be like if Google had disallowed Java and had written everything in Lisp instead.
- pchristensen 18y ago
  I do recall Norvig saying that they use C++ for a lot of core code because even though Lisp would be cheaper to develop, they run so many servers that any decrease in efficiency would cost millions (can't find the quote though)
  - jrockway 18y ago
    If making lisp run faster would save someone millions of dollars, lisp would run faster. Sure, it's practical for Google to use C++ in this case [1], but I am imagining a fantasy world. [1] Unless of course bugs that C++ ignores would be caught by Lisp. Perhaps there is a minor type error in Google's code that makes the search results not quite as good. If CL's type checker caught that, they would have gotten super-rich sooner and would own Microsoft right now. But like I said, this is all fantasy. My real argument is "You are not Google."
    - silentbicycle 18y ago
      Making Lisp run faster would almost certainly involve making it closer to SML / OCaml. Beyond algorithmic changes, speed optimization in Lisp usually involves type declarations, or sometimes inference, as in ML. (See: http://www.lrde.epita.fr/~didier/research/verna.06.imecs.pdf http://www.lrde.epita.fr/~didier/research/verna.06.imecs.pdf) Give Lisp a really powerful, inferred static type system and you're most of the way there. (Give it a better module system, while you're at it.) And if you want to talk about a type checker catching bugs... I wish OCaml had kept the s-expression syntax, but it's a very interesting (and powerful) take on improving Lisp. (I think it also helps that they don't call it Lisp. It flies under the radar as far as Lisp's reputation.)

logjam 18y ago

"The situation is particularly ironic because the argument that has been advanced for discarding Lisp in favor of C++ (and now for Java) is that JPL should use "industry best practice." The problem with this argument is twofold: first, we're confusing best practice with standard practice. The two are not the same." To me, this is the crux. We have this ridiculous idea that "industry" drives technological advance. Industry software "engineers" trained up in trade schools or worse, without any awareness that they are reimplementing solutions (poorly) to problems that were solved decades ago...and we get...horrible industrial monstrosities like Java (and Microsoft Windows) roaming the earth, while remote diamonds like Lisp and Scheme shine kindly down.

silentbicycle 18y ago
"Come on, dude. You can't argue with best practices. They're the best!" Which is the problem, I think. Their name just screams, "Quit arguing, they know better." (for increasingly nebulous values of 'they'). Aside from trying to undermine the term as a brand ("Best Practices: Because Embracing Mediocrity Looks Good On Paper"), what can you do?
DaniFong 18y ago
Java wasn't that crazy. The basic idea of using Java for the web seemed a sane one: the only other alternative was to do something like XWindows. And then what? Are people going to use web browsers like XWindows clients? That would never fly! (oh wait)
briancooley 18y ago
Industry software "engineers" trained up in trade schools or worse, without any awareness that they are reimplementing solutions (poorly) to problems that were solved decades ago...and we get...horrible industrial monstrosities like Java Since Guy Steele coauthored both the Lambda Papers (late 1970's) and the first three editions of the Java specification, I don't think that you can successfully argue that awareness of anything solved by Lisp or Scheme was a problem in the development of Java. I always got the impression that the goal with Java was to make bad programmers better, not to create the ultimate language (e.g., see http://fishbowl.pastiche.org/2004/03/17/halfway_between_the_gutter_and_the_stars/ http://fishbowl.pastiche.org/2004/03/17/halfway_between_the_...) To use a golf analogy, consider cavity back irons. The average golfer, who struggles to hit it straight, will likely play a lot better with cavity backs. But a really good golfer won't be able to shape shots easily and will feel hamstrung without his blades.

DaniFong 18y ago

In the words of Elton John: It's sad. So sad. It's a sad, sad situation. My best hope at this point is that the dotcom crash will do to Java what AI winter did to Lisp, and we may eventually emerge from "dotcom winter" into a saner world. But I wouldn't bet on it.

ph0rque 18y ago

lisper 18y ago
I quit JPL and started a new career as a VC :-)
- ced 18y ago
  Do you have that written out in another post somewhere? I loved this one.
  - lisper 18y ago
    Nope. I haven't been doing it long enough to have gotten any good stories out of it yet. I did write this a while back, which was a big hit in its day: http://rondam.blogspot.com/2006/10/top-ten-geek-business-myths.html http://rondam.blogspot.com/2006/10/top-ten-geek-business-myt...

zandorg 18y ago

Lisp at the very least is excellent for initial prototypes.

gibsonf1 18y ago

Is it just me, or is the idea of using a repl on a computer in space simply fascinating?

bayareaguy 18y ago
What I found more interesting was this section in the story of the Remote Agent bug ( http://ic.arc.nasa.gov/publications/pdf/2000-0176.pdf http://ic.arc.nasa.gov/publications/pdf/2000-0176.pdf ) One of the errors found with SPIN, a missing critical section around a conditional wait statement, was in fact reintroduced in a different subsystem that was not veriﬁed in this ﬁrst preﬂight effort. This error caused a real deadlock in the RA during ﬂight in space. So the bug fixed with the repl was actually one that was uncovered by the SPIN verifier ( http://spinroot.com/spin/whatispin.html http://spinroot.com/spin/whatispin.html ) months prior to the launch, but wasn't fixed because they didn't verify the code they actually decided to use.