← Back to context

Comment by Animats

12 years ago

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.

13 comments

Animats

Reply
mafribe  12 years ago

It's still too slow today for all but the most security critical applications.

Fortunately there is a lot of work in progress to improve the situation.

  • tempire  12 years ago

    It's not too slow, it just takes discipline that most developers/companies don't have, primarily because the tools aren't widely available.

    • AKluge  12 years ago

      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.

      1 reply →