I encountered HOS back when I was doing proof of correctness work, and didn't really understand how it got beyond very simple problems. But I thought, at the time, that was my fault. In retrospect, it's an approach for a certain class of control problems dominated by required relationships between certain variables. That's what flight control systems are all about.
Control problems are typically expressed as a set of "laws", equations which define what's supposed to be happening given the inputs and perhaps past inputs. Some of these are equations, and others are constraints. Checking those laws for contradictions and turning those laws into code is partially automatable, and that's what HOS was trying to do.
HOS only seemed to work well with the founders driving it. Somehow, they were never able to express clearly what they were doing. Sometimes that happens. Norm Hardy, who came up with capability-based systems and created KeyKos, a capability-based OS for IBM mainframes, had that problem. The system worked great, but nobody understood what he was doing. He used to have an "explainer", Susan Rajunas. In both cases, the startups went bust.
Trying to get people to understand a complex formal system is very hard. Harder than developing one.
[1] http://www.dtic.mil/dtic/tr/fulltext/u2/a198753.pdf [2] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD08xx/E... [3] https://news.ycombinator.com/item?id=8736450