Yes, she was one of the early formal-methods people. I met her and Saydeen Zeldin back when I was doing proof of correctness work. They had a company called Higher Order Software, which promoted an extreme form of waterfall design using formal methods. This is appropriate for avionics but didn't catch on. Proof of correctness was just too slow back then.
Incidentally, when you post articles like this, please don't use a title that makes it sound like an obituary.
Having learned and put into practice formal proofs of correctness at CMU, I can say that it has fundamentally improved the discipline with which I write production code. The undercurrent of "Is this provably correct" is still there 30 years later, and it produces better code than the more obvious "Will this work here". The cost in production time is small compared to the later revision, refactor and maintenance issues.
I wonder if we are talking about the same things. Do you use Hoare logic or interactive proof assistants when putting "nto practice formal proofs of correctness", and find that that lowers your software engineering costs? I would be surprised if that was the case.
I haven't used Idris, but as a proof assistant, Coq is one of the best computer games I know[1]. As a programming language, it's a very good proof assistant.[2]
[1] Really! It's fun. I've found the resulting proofs impossible to read, though. The closest description I can make is that they're programs for a stack machine; reading those is not a skill I've developed.
[2] All of the dependently typed languages, like Coq, that I've seen have not been very good programming languages, in my opinion. Except for ATS, which I don't think is a good programming language for different reasons. But I really like it, anyway.
> All of the dependently typed languages, like Coq, that I've seen have not been very good programming languages, in my opinion.
Yeah, that's why I'm looking at Idris - it seems like the only one that's oriented towards practical programming. I did eventually get it installed, but it's tough going doing anything with it when you don't know Haskell tbh.
> Idris - it seems like the only one that's oriented towards practical programming
Whether you like ATS or not, it's very oriented towards practical programming. Also, ATS mostly looks bad IMO because of the style the author uses.
I still haven't fully formed an opinion on ATS though. Idris does seem really cool and stuff like enforcing time/space usage through the type system excites me.
I'm not sure whether my issue with ATS is the style of the author or its type system, although I suspect the former.
ATS is based on ML (the author started with Dependent ML), but the code has a very imperative feel, leading to statements like "let () = expr() in ..." and "let x = ... in ()".
Here's just a small translation of the ats examples[0] page.
-----------------
Copying File
----------------
Authors version:
fun
fcopy (
inp: FILEref
, out: FILEref
) : void = let
val c = fileref_getc (inp)
in
if c >= 0 then let
val () = fileref_putc (out, c) in fcopy (inp, out)
end // end of [if]
end (* end of [fcopy] *)
fun fcopy (
inp: FILEref,
out: FILEref
) : void = let
val c = fileref_getc (inp)
in
if c >= 0 then let
val () = fileref_putc (out, c) in fcopy (inp, out)
end
end
Authors version:
fun
fib (
n: int
) : int =
if n >= 2 then fib (n-2) + fib (n-1) else n
My Version (not sure if valid!):
fun fib ( n: int ) :
int = if n >= 2 then fib (n-2) + fib (n-1) else n
-----------------
Fast Fibonacci
----------------
Authors Version:
fun
fibc (
n: int
) : int = let
fun loop (n: int, f0: int, f1: int) =
if n > 0 then loop (n-1, f1, f0+f1) else f0
// end of [loop]
in
loop (n, 0, 1)
end // end of [fibc]
My Version:
fun fibc ( n: int ) : int =
let
fun loop (n: int, f0: int, f1: int) =
if n > 0 then loop (n-1, f1, f0+f1) else f0
in
loop (n, 0, 1)
end
I worked with Margaret and Saydeen at Higher Order Software for my first job out of college, but I didn't get to work on anything as glamorous as Apollo. We did mostly government contracts; I was there for two years before I decided it was time for grad school.
Is HOS what it seems? I read about it years ago in "System Design from Provably Correct Constructs". It seems like it should revolutionize software development (and incidentally put most programmers out of business) but that it somehow just never gets "traction" beyond certain markets/customers?
The first time -- and still one of the few times -- I ever walked out of a meeting because the BS level seemed too high was when I visited Higher Order Software in the 1980s.
Can you please share details of what caused you to walk out? There is a lot of curiosity around USL and the toolchain she and her team have built, but my Google-fu has failed to come up with descriptions of practical experience with them. I'm struggling to decipher how different it is from UML, or what it is solving that functional approaches are not already working to address.
It was 30ish years ago, so I don't recall details. But it seemed overhyped. The usual problem with tools that do a great job of generate code is that they do a great job of generating CERTAIN KINDS of code, but are unhelpful or even counterproductive with other parts of your development task. Certainly this was true in the 1980s, and back then the problem was exacerbated in that there weren't graceful ways to combine what was generated with what you had to write or modify by hand.
I find it a bit... sad? disturbing? that the only reason women were so involved in computing and programming in the early years was because programming and software were seen as less important jobs than the "software planner" jobs, where the "coder" was just a flunkie, something of a software custodian. They were considered clerical jobs, like data entry or a secretary.
This old article (2009) has a lot more details on this old sociological phenemonon:
I started programming before I was a teenager, in part because my mother was a programmer. At that time, 30+ years ago, women were not programmers because it was "less important". You didn't see men taking programming jobs as a "Consolidation" for some better career.
My first two programming teachers- in college and in high school- were both women who were also professional programmers at previous jobs.
It was a prestigeous job, as the computer was seen to clearly be the herald of a new age. The personal computer revolution was really significant. It was a job for smart, mathematically inclined people.
I think programming is seen as a lower status job now than it was then. Now programmers are subservient to ignorant business people (When the reality is, its much easier for use to learn business than them to program.)
I think in the past women were more likely to be programmers because the profession didn't have a gender stigma. Because men were more likely to have picked out a profession, and women who entered college without a specific degree plan were more likely to pick this one up.
And frankly, I've never seen a problem with women programmers. I've worked with women programmers at every job where there were more than 10 programmers, and they haven't been seen as deserving, or treated with less respect... this goes back to the 1980s.
I would like you to back up your assertion that the "only reason" they were involved was low status. That paper you linked to is fallacious beyond belief. You may disagree with my anecdotes below, but he's merely giving us his spin on an article. (So he's not only anecdotal, but derivative.)
If you're going to make a list of people that John von Neumann looked down on, it's going to be rather longer than just women (try anyone who wasn't as smart as he was, which is just about everyone).
>because programming and software were seen as less important jobs than the "software planner" jobs,
It's not like STEM software today like the codebase of ATLAS for example, is give much praise in the public eye. It's simply overshadowed by the larger more ambitious project that it was part of. This was the case back then as well.
Her site has a pretty neat article called "Inside development before the fact":
> Today's traditional system engineering and software development environments support their users in "fixing wrong things up" rather than in "doing them right in the first place". Things happen too late, if at all. Systems are of diminished quality and an unthinkable amount of dollars is wasted. This becomes apparent when analyzing the major problems of system engineering and software development.
Also a cool paper she wrote:
> The key to software reliability is to design, develop, and manage software with a formalized methodology which can be used by computer scientists and applications engineers to describe and communicate interfaces between systems. These interfaces include: software to software; software to other systems; software to management; as well as discipline to discipline within the complete software development process. The formal methodology of Higher Order Software (HOS), specifically aimed toward large-scale multiprogrammed/multiprocessor systems, is dedicated to systems reliability. With six axioms as the basis, a given system and all of its interfaces is defined as if it were one complete and consistent computable system. Some of the derived theorems provide for: reconfiguration of real-time multiprogrammed processes, communication between functions, and prevention of data and timing conflicts.
Besides the great photo and backstory, I liked this snippet:
> She was all of 31 when the Apollo 11 lunar module landed on the moon, running her code. (Apollo 11 was able to land at all only because she designed the software robustly enough to handle buffer overflows and cycle-stealing.)
You could read that paragraph in several ways. Back then, accomplishing something like that at 31 seems precocious. Today, in the hype about 18-year-olds becoming millionare-startup founders, she sounds like a late bloomer of a programmer.
Considering she didn't learn how to program a computer until her 20s, and there were no shoulders of giants (sorry, frameworks and operating systems) to stand upon, I'd say it's a more impressive feat.
Some years ago, there was a video about the moon landing in Washington DC airport (it was at a Smithsonian exhibit or store or some such). It included video of the control room when the alarm went off during descent. There was silence and blank faces - nobody knew what to do.
But by the time the alarm went off the second time on descent, it was completely different. Someone - whoever was in overall charge - called a role (something like "descent control officer") and that person responded "go", all within one second.
But, yes, it wasn't a problem because the priority scheduling recovered from this problem, and that recovery was a really big deal.
> Some years ago, there was a video about the moon landing in Washington DC airport (it was at a Smithsonian exhibit or store or some such). It included video of the control room when the alarm went off during descent. There was silence and blank faces - nobody knew what to do.
You have to be careful interpreting something like that. Without the backstory, you run the risk of projecting your own emotions onto the events.
Mission Control was actually not very worried about the program alarms. According to Gene Kranz in his memoirs, the white team had been fed a program alarm during a pre-flight simulation. In fact, it was the last simulation they ran through before launch, so it was fresh in their minds.
During the simulation, Mission Control incorrectly called an abort. During the debrief, the instructors told them that the program alarm was non-fatal, and they should have continued to a lunar landing.
During the actual lunar landing, Mission Control was astonished to run into the same scenario. It was like running through the simulation a second time.
> But by the time the alarm went off the second time on descent, it was completely different. Someone - whoever was in overall charge - called a role (something like "descent control officer") and that person responded "go", all within one second.
Neil Armstrong did have to ask twice, but he did get a response from Mission Control on the first alarm. Mission Control did not ignore the first alarm.
The delay was caused by having to consult a list of fatal and non-fatal program alarms. Once they had that list, it was easy to call a Go on subsequent program alarms. However, they couldn't just give a Go to the first alarm without checking the list.
Armstrong and Aldrin hadn't participated in that earlier simulation, so they were probably a lot more worried than Mission Control was!
Wasn't that the same alarm that was randomly thrown at the astronaughts in training and they made the wrong choice then and learned to make the right choice on the moon?
I will look up the story in Kranz's autobiography when I get home tonight.
I do believe it was. The Simsups threw a 1201 alarm at them, and the controllers got confused, and Kranz called an abort. Afterwards, they told him, "It wasn't an abort, you should have continued the landing...I thought you guys had it, but then you went off the rails and called for an abort...You violated the fundamental rule of Mission Control: You must have two cues before aborting. You called for an abort with only one! " As a result, one of the controllers went more into depth on program alarm codes, and they put a rule in dealing with which alarm codes would be grounds for an abort. Neither 1201 nor 1202 were on that list. They saw both those alarm codes during Eagle's descent, and were able to say, "We're Go on this alarm...we're still Go, same type, it's a Go." And the rest was history.
See, I see this and the other photo of her as conveying the message, "You don't have to look like the stereotypical 'NASA nerd,' the white guy with the white button-down shirt and the pocket protector full of pens, in order to make a contribution. Some of the biggest contributions were made by people who didn't fall into that stereotype."
Feats of engineering, while technically within the definition of "application" like virtually every other artifact of deliberate human action, rarely actually get described as such.
It looks like she is currently CEO of a company that sells a formal-methods language (and accompanying IDE) called 001. It looks interesting - has anyone here worked with it before?
"Many of the things I was intrigued by had to do with how to make the mission software safe and reliable. And one of the things I remember trying very hard to do was to get permission to be able to put more error detection and recovery into the software. So that if the astronaut made a mistake, the software would come back and say "You can't do that." But we were forbidden to put that software in because it was more software to debug, to work with. So one of the things that we were really worried about is what if the astronaut made a mistake -- We were also told that the astronauts would never make any mistakes, because they were trained never to make mistakes. (Laughter)
So we were very worried that what if the astronaut, during mid-course, would select pre-launch, for example? Never would happen, they said. Never would happen. (Laughter) It happened."
She also mentions her companies:
"So since that time, the theory has evolved and now I actually lost the first company to venture capital people, and started a second company called Hamilton Technologies."
Interesting, and something I didn't know. The cited source unfortunately doesn't elaborate on the context. The chronology does seem about right. The first in-print use of the term I can find is from 1969, when it was used as the title for the proceedings of an October 1968 NATO scientific conference: http://dl.acm.org/citation.cfm?id=1102020. Given the NASA/NATO personnel overlap at the time, it's certainly plausible that they got it via NASA.
She was briefly mentioned in Steven Levy's "Hackers", as an MIT computer user who's program crashed after the "Midnight Wiring Society" changed how the computer worked.
Also, she was interviewed in "Moon Machines" episode three, about the nav computer.
Both female and male computer scientists need good female role models, and for the same reasons. In my own life I've been very fortunate to have been influenced by my mother (who taught me to program at an early age), by a grade school computing teacher (who also encouraged me to learn programming), and by my wife (a professional software engineer, among other things). I like to think that my wife's professional career has given my kids some similar perspective - even if only to change their unconscious assumptions about what women can do (which is everything, since my wife has been a writer, a software engineer, a business analyst, and a small business owner - and that's just what she's done professionally). Women needs to believe that they're capable of everything, and men need to believe that women are capable of everything, too. The same goes for men about men, and women about men. Feminism isn't about replacing patriarchy with matriarchy. It's about egalitarianism for all genders. That's all I meant.
I just copy and pasted the article and attached the photo to an email to my 1 year old daughter. I have an email account for her for just this kind of thing. I can only hope she's as inspired by it when she grows up and reads the emails as I hope she will be :)
What a truly inspiring human being. I can only dream of aspiring to her levels of contribution.
Check out some of the Apollo 11 code for the Lunar Module's (LM) Apollo Guidance Computer (AGC). It's just awesome browsing through it, reading the comments, and thinking about the zeitgeist of being on a team that was working on something of that world-altering magnitude.
"There was no second chance. We all knew that. We took our work very seriously, but we were young, many of us in our 20s. Coming up with new ideas was an adventure. Dedication and commitment were a given. Mutual respect was across the board. Because software was a mystery, a black box, upper management gave us total freedom and trust. We had to find a way and we did. Looking back, we were the luckiest people in the world; there was no choice but to be pioneers; no time to be beginners." - Margaret Hamilton
- - -
Edit: OK, this is interesting. Note the filename. The filename and comments suggest that it was for driving keyboard and information display...
According to wikipedia
"The onboard guidance software used a Kalman filter to merge new data with past position measurements to produce an optimal position estimate for the spacecraft."
https://en.wikipedia.org/wiki/Apollo_PGNCS
In turn the main source of navigation information came from mission control using least squares. A source on that would be nice too!
A lot of people will find it hard believing how smaller code can be in assembly than in our supposedly higher level languages, e.g, look at this example of quicksort, http://en.wikibooks.org/wiki/Algorithm_Implementation/Sortin...
go down to the C example below and note that it's longer.
The scalar case is not so bad; typically the filter is taught using the vector-input/vector-state case, which is more complex.
I can't make heads or tails of the assembler listing either. The specific thing I would look for in the assembler code is the division operation which is required to find the Kalman gain. I don't see it.
The amazing thing from my point of view is not the implementation. It is rather that the theory, which was quite novel at the time, was only understood and published in 1960/61. To have it used in a flight system, and indeed a manned flight system, only 8 years later is really incredible.
When this story was posted yesterday [1], the comment about UDL sparked my interest. That led me to Hamilton'sDevelopment Before the Fact methodology [2]. I find DBTF an appealing approach to reliable systems, particularly buildings. Because AEC design software is largely focused on automating manual steps rather than the generation of systems.
In early computer days a fair fraction of the programmers were women. They migrated from earlier computer jobs such as keypunch operators, switchboard wirers (some early computers had programable switchboards) and mechanical calculator clerks. Until mid 1940s "computer" meant the third category- a person who operated mechanical calculators.
I hope this serves as tangible evidence that women do have their place in tech. I feel it's a shame that we believe (rightfully or not) that we need extra coding schools for females.
This kind of comment has no place and is irrelevant, IMHO. Even though the statement may be well-meaning, it's completely gender biased.
How many times in an article about a male entrepreneur, or computer scientist, or other interesting person, is his subjective physical attractiveness even a topic of conversation? Almost never - and that's the way it should be for everyone.
Here's a short list, some very legitimate sources that are linked on HN all of the time, that mention Elon being 'sexy', along with a Google search query link for 'Elon Musk handsome' to get a host of other examples.
I can see commenting about a stranger's physical appearance if they're dressed in a surprising way (if somebody shows up at a tech conference in a tux or evening gown, or dresses in a costume, it's reasonable to expect some degree of attention.) I can see commenting if they have known health problems they're recovering from (like late in Steve Jobs' life.) And I can see commenting if someone appears to be considerably younger or older than they actually are [0] (when I was a teen and my parents were in their late 40s or 50s, people occasionally asked if my dad was my brother or my mom was my sister or girlfriend.) Those kinds of comments can be gender-neutral and non-harassing, and furthermore genuinely interesting points of conversation. But we should definitely stay away from creating the impression that physical attractiveness is one of the most important qualities for women in tech, or almost any other professional context.
>How many times in an article about a male entrepreneur, or computer scientist, or other interesting person, is his subjective physical attractiveness even a topic of conversation?
All stories about Elon Musk in the mainstream media.
Yet Elon Musk is remembered is remembered and regarded as an entrepreneur, not as as a physically attractive person. Contrast this with women who are regarded as "sex symbols" and you'll see that their physical appearance is used to overshadow and demean their achievements.
> How many times in an article about a male entrepreneur, or computer scientist, or other interesting person, is his subjective physical attractiveness even a topic of conversation? Almost never - and that's the way it should be for everyone.
I don't know, I would have liked advance warnings for some blokes who turned out disturbingly attractive, making their talks harder than necessary to follow.
If the tech field were evenly split 50/50, do you think women wouldn't comment on the attractiveness of guys?
Maybe, but how would that make a person's (of either gender) physical attractiveness (which is completely subjective, by the way) relevant to a discussion of an article about their technical accomplishments?
You're basically saying "We may, in a hypothetical future, have two wrongs", but remember that 2 * wrong != right.
People have been mentioning that sometimes there are discussions of male entrepreneurs or technical folk that comment on their appearance, but I like to think that HN is above that level of discourse.
The claim was that stating this woman is attractive is "gender biased". My point is that there is no gender bias as shown by women doing the same thing. Aside from the dubious claim of gender bias, "badness" has not been established.
Physical attractiveness is not "completely subjective". There are very well established body proportions, symmetries, and other physical indicators of human attractiveness that are consistent across cultures and throughout time.
If I were gay, and I saw an unusually attractive (male) entrepreneur or programmer or whatever, I'd probably mention it as well. It's not sexist when it's equally balanced to men and women.
(However, given the demographics and percentages - male/female, straight/gay - you're going to get a lot more straight men commenting on women's looks in this sort of area.)
Incidentally, when you post articles like this, please don't use a title that makes it sound like an obituary.