Name: System design from provably correct constructs
ISBN: 9780138814830

What Hacker News says

nickpsecurityApr 2024

I had to dig it up out of my order history for you. Here is the HOS book. I've included a preview link that shows the Table of Contents.

System Design from Provably Correct Constructs: The Beginnings of True Software Engineering by James Martin https://www.amazon.com/gp/product/013881483X/ref=ppx_yo_dt_b...

https://archive.org/details/systemdesignfrom00mart/page/n3/m...

Now, if you want a practical method, the best were Design by Contract, Cleanroom Software Engineering, and Praxis' Correct by Construction. Cleanroom and CbyC hit very, low, defect rates. DbyC was highly pragmatic in balancing developer productivity, ease of adoption, and correctness. I think they'd all be even better combined with functional programming, static, test generators, etc. that we now have. In any case, here's links to descriptions of and books on some of those methods.

Design by Contract article https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-b...

Overview of Cleanroom Method https://ifs.host.cs.st-andrews.ac.uk/Books/SE9/Web/Cleanroom...

Book teaching Cleanroom https://www.amazon.com/gp/product/0201385953/ref=ppx_yo_dt_b...

Overview of Praxis Correct by Construction https://elsmar.com/pdf_files/A%20Manifesto%20for%20High-Inte...

Book teaching SPARK Ada with some CbyC https://www.amazon.com/gp/product/1107656842/ref=ppx_yo_dt_b...

Abstract, State Machines and the B Method had many successful, industrial uses. There's many papers on them.

thread

carapaceAug 2022

You might like "System design from provably correct constructs", it's written by James Martin but it's presenting the work of Margaret Hamilton. She developed the ideas while working on Apollo 11

https://archive.org/details/systemdesignfrom00mart

In modern terms it works by allowing the user to edit a kind of abstract syntax tree (without the syntax) using only operations that preserve correctness (essentially type checking) so you literally can't make a bug. (You can still make a program that does the wrong thing correctly.)

The four essential operators are (of course) sequence, branch, loop, and parallel (non-interference).

(As you note, state machines are useful for describing complicated systems, but they themselves are simple in terms of the four operations.)

thread

carapaceMar 2022

Ah! Gold!

I found Hamilton's work described in a book “System Design from Provably Correct Constructs” https://archive.org/details/systemdesignfrom00mart many years ago. You build something like an Abstract Syntax Tree using operations that preserve certain correctness properties, thus eliminating many categories of bugs. It grew out of her work on Apollo 11.

She's credited with coining the term "software engineering".

thread

carapaceJul 2019

I'm folding in responses to your other comments here. Well met BTW.

- - - -

You found Dijkstra's review. I'm a fan of his but the guy was hugely arrogant. IMO he craps on them pretty harshly.

I can kind of see where he's coming from, but "he doesn't get it" IMO. He misses the point (or maybe HOS sucked compared to what was later described in Martin's book...)

- - - -

FWIW, James Martin went on to write "System Design from Provably Correct Constructs: The Beginnings of True Software Engineering" which is where I learned about all this. I don't actually know much about HOS specifically, only what's in that book. If you're interested that's the thing to read.

- - - -

> So how does this prevent any bugs which aren't already prevented by the language?

The UI would not let the user enter syntactically nor semantically incorrect "trees".

In modern terms, if you had a syntax-oriented editor (like Alice Pascal) for a language with good type-checking I think you would have most of what HOS et. al. was or did. At the time of Apollo 11 (circa 1969), type-checking was barely a thing:

> In 1969 J. Roger Hindley extended this work and proved that their algorithm always inferred the most general type.

https://en.wikipedia.org/wiki/Type_inference#Hindley%E2%80%9...

- - - -

> Equating the most trivial kind of errors (which are caught by the compiler anyway) with "all sources of bugs" ignores the kind of bugs which are actually hard to prevent and might slip into production.

Yes, I know, sorry. I admitted that "all sources of bugs" was hyperbole. I was going for rhetorical effect.

> caught by the compiler anyway

First, why wait? If the errors cannot be committed in the first place surely that's better than detecting them only at compile-time?

Second, compilers didn't catch those errors back in the day. The whole reason Dr. Hamilton made up this stuff was because existing methods, tools, and technology would have crashed her spaceship.

> ignores the kind of bugs which are actually hard to prevent and might slip into production

Every moment saved by the machine is a moment the humans can use to prevent or detect the errors the machine can't detect automatically.

Here we are back to Dijksra. You know he only got a physical computer when his colleagues forced him to get a Mac so they could email him, eh?

He held, and I agree, that the kind of errors you're talking about do not happen while typing in the software. They occur "between the keyboard and the chair". If I may wiggle a little, I think of "bugs" as glitches in the machine, while the kind of errors you're talking about I think of as just "errors". But I know that's idiosyncratic, and that most people lump them together as just "bugs".

The only thing you can do about them is think clearly.

- - - -

The original question of this subthread was, "What is software engineering, anyway?"

My answer is, "What Margaret Hamilton did."

My point is that we have had tools that systematically eliminate sources of error. All automatically preventable bugs should be prevented (modulus economic consideration, but here costs would be trivial for automation of error prevention and the benefits and cost saving would be pretty high.)

Otherwise, calling ourselves "engineers" is pretty lame. IMO.

- - - -

> If you want to interest people in these ideas, you should show how it can solve real problems.

Real problems, eh? :-) Sending a spaceship to the moon? And getting it back? And no one died?

https://en.wikipedia.org/wiki/Apollo_Guidance_Computer#PGNCS...

To be fair, I don't know to what degree J. Halcombe Laning's software was influenced by Hamilton. She's pictured next to the "software" section of the Apollo Guidance Computer Wikipedia article, but not mentioned.

> The design principles developed for the AGC by MIT Instrumentation Laboratory, directed in late 1960s by Charles Draper, became foundational to software engineering—particularly for the design of more reliable systems that relied on asynchronous software, priority scheduling, testing, and human-in-the-loop decision capability.[14] When the design requirements for the AGC were defined, necessary software and programming techniques did not exist so it had to be designed from scratch.

https://en.wikipedia.org/wiki/Apollo_Guidance_Computer#Softw...

- - - -

FWIW I suspect that these folks are going to be the coming cutting edge (of true software engineering): https://www.categoricaldata.net/ ... fallout from Applied Category Theory http://www.appliedcategorytheory.org/

thread

carapaceSep 2018

> I hope you succeed, and I say that sincerely

Cheers! Me too. (^_^)

Brother, I really don't want to have this argument again. I don't care anymore if my peers believe me or not. I'm just going to bring it to market as best I can and see how it goes. Thank you for the well-wishing, and I apologize again for being so cranky.

A few lil points:

> I'm not aware of any support for your statement that "error-free software development methods have been available for decades" for any reasonable definitions of "error-free" or "available".

I know. You are making my point: The methods are there, and no one has ever even heard of them.

The primary method I am talking about was developed by Margaret Hamilton during the Apollo 11 mission to the Moon, and she has unsuccessfully marketed ever since AFAIK. Dijkstra once reviewed it and panned it harshly. It was a rare case of him not getting it. It went right over his head.

Hamilton, by the way, is the person who first coined the term "Software Engineering".

I'm not going to go into it further now, suffice it to say if you are typing text into a text editor to write code you are doing it wrong. There's a book, "System Design from Provably-Correct Constructs" by James Martin, that presents Hamilton's method if you're interested.

> The whole point of the original article is that, today, the only thing keeping planes in the air is fault tolerance and lots of redundancy (see also: Erlang). Assertions are about humility and it's good to be humble.

Planes stay in the air because they are designed to survive the failure of the individual parts. Now I would never suggest that proven-correct software cannot fail. Of course it can. Need I invoke the Cosmic Rays? I heed Murphy.

But you only write an assertion if you're not certain, eh? You're saying, in code, I think this will never ever happen, so if it does STOP-THE-LINE.

That kind of uncertainty is absurd, inexcusable, in software. (One of the very few realms that this is true, Herr Gödel notwithstanding. Software is electrified math, math is the "Art of What is Certain".)

I'm saying that our current common methods of software development are pathetic, that we are working far too hard to write software with far too many bugs, and it doesn't have to be this way. I'm further saying (to the OP) not to waste breath arguing with folks who can't or won't even accept the possibility! I've been doing it for a few years now and it's thankless. I've managed to convince exactly one other person and he's a brilliant programmer who came to it from a background in philosophy. He's a thinker rather than a puzzle-addict or complexity junkie.

Anyhow, if I manage to bring this thing together I'll make a noise here on HN (despite YC getting into bed with the Chinese Communists, the greedy fools.)

> On one hand you seem to suggest that error handling is bad because there shouldn't be errors (what about I/O? user error?) while on the other hand you seem to be defending the position that monadic error handling is a panacea.

Nope. Nothing like that. I can't explain it all her and now, but uh... Have you heard of Elm-lang? They boast zero front-end errors. Zero. The Elm compiler makes the JavaScript and it does not error. They do not write "error handling" to achieve this.

thread

carapaceJul 2018

> Based on empirical evidence, there isn't really a problem at all with the way people program.

I disagree strongly. I would say that software development is a tire fire. Every day there are reports of bugs in software causing all kinds of real-world problems. These days software bugs can kill people[1]. And there are only going to be more CPUs and more software and more bugs going forward.

> Markets have already mostly figured out the rare cases when such robustness is really needed.

I don't see how this is a supportable statement in a world that includes the "Toyota Unintended Acceleration" bug? (Among so many many others.) When you say, "a perfect solution according to markets is the solution that does the job for the lowest cost over time" aren't you effectively saying we should only expect software to be as good as has to be to protect the liability of some corporation? Not to take a cheap shot, but uh, I think the families of the people who died in the car accidents-- excuse me, collisions ("'Accident' implies there was no one at fault.") --might have a different attitude to software correctness?

In any event, your entire argument is predicated on the idea that correct software is expensive. But this is only true because we, as an industry, have not made effective use of the the available tools to write correct software!

It's not expensive to write correct code. It doesn't take longer either. We just don't do it.

Dr. Margaret Hamilton figured out how to write bug-free software as a side effect of her work on the Apollo 11 program years ago and nobody noticed.[2] (She's the person who coined the term "Software Engineer" BTW.) Byte-for-byte, flawless code is no more expensive than buggy code. And maintenance costs are near zero, so it's actually cheaper. You just have to use the right method (which has existed for about 30~40 years, nearly totally ignored.)

Please PLEASE don't make excuses. We've can get this right, even if "the market" doesn't notice or care.

To reuse my lumberjack metaphor from my other comment: Chainsaws exist. They are safer and faster than axes. There is in fact no way that cutting down trees with an ax is objectively better than cutting down trees with a chainsaw.

You are maintaining that, since trees are felled well enough with axes today, there's no sense in investing in chainsaws and chainsaw training, not now, nor ever in the future.

You're saying that "the market" only really needs wood cut by axes and doesn't value wood cut by chainsaws because all the furniture made with it is good enough, and we should just live with splinters and chairs that break and drafty houses, etc...

Frankly, it's kind of a lame argument to find on a pro-tech forum. Fancy sophisticated technology is awesome, unless it threatens to obsolesce your favorite ax, eh?

> you have to be able to find qualified developers, and what developers learn is based on popularity and fashion.

This is the source of the problem: we're not "engineers", we're not even car mechanics! We're barely above the level of kids building go-carts in their backyards out of junkyard parts. We should be ashamed of our fashion-driven-ness. The amazing thing is that we got the business people to go along with this![3]

Maybe someone should just start offering chainsaw-cut wood at cheaper prices than the hand-hewn crap and see if "the market" likes that noise? (In case I'm being too arch, that's exactly what I'm about right now. I'm so freaking passionate about this.)

"Program correctness" shouldn't have to be "top priority" because it should be the default. You should get it "for free" along with the software for the same price because it costs nothing extra.

[1] For example: "A Case Study of Toyota Unintended Acceleration and Software Safety" Prof. Phil Koopman. September 18, 2014. Carnegie Mellon University https://users.ece.cmu.edu/~koopman/pubs/koopman14_toyota_ua_...

[2] Nearly nobody noticed. I know it sounds crazy but it's true: There's a simple, easy method to develop bug-free software. James Martin wrote it up in a book "System design from provably correct constructs: the beginnings of true software engineering." in 1985. That's probably the best source if anyone wants to read up on it.

[3] A programmer in language or framework A who cannot or will not learn language or framework B is not a good programmer. (I don't mean putting "Won't do PHP" on your resume, I mean that you can't or won't learn it in the first place.) Q: "What if we can't find Python devs? There are so many Java devs. We should use Java." A: "Why would you hire a Java guy who can't do Python? Even to do Java?" I've had that conversation a bunch of times.

thread