"Interesting discussion, I'd be keen to try such a formalistic approach if you ever have a need for a remote critical eye."

I'll try to keep it in mind. There's a few people doing stuff in public if you want to play with it. Plus lists to stuff to try. Here's a few.

One person did an overview of Cleanroom and examples in Python, etc here:

http://infohost.nmt.edu/~shipman/soft/clean/

I just pulled a list of techniques that were empirically proven to increase robustness into a Pastebin:

http://pastebin.com/xZ6m4T8Z

Note: One can pick and choose among these to find right work/benefit ratio. I'd like to see lots of experiments on mainstream software to get data on what's 80/20 rule. I'm betting on sane subsets of safe languages, code reviews, usage-driven testing, interface checks (even asserts), and fuzz testing maybe. The first four are widely available and take little work.

Case study of Altran's Correct-by-Construction approach showing great metrics:

https://www.commoncriteriaportal.org/iccc/7iccc/t1/t1201100....

Note: Altran does plenty of medium and high assurance work. Their method can do either. I'd rate Tokeener as Medium-High if just focusing on their part of it. Note that they got it done with 3 part-timers in less than a year with code-level proofs. Quite a leap from millions spent on teams of geniuses doing proofs in Gypsy, etc two years at a time back in the day. :)

"Regarding the quote, I don't think you quite took the spirit of it: the idea is that, given a replaceable component with failure expected, we can manage reasonably to achieve the same outcomes for less overall cost "

I'm not questioning the spirit so much as the implementation.

" do not build the one true system to solve all availability and security challenges (which would be very expensive (the old "pick two" adage)), but rather build a system which makes use of the properties of components intelligently to reduce overall hassle"

That's what I advocated. With medium assurance, it cost almost nothing extra so apply it to the components. With high assurance, if used at all, it can be used on just the most important and is by some niche players with good cost/benefit results. It's just that...

"to achieve the same objectives, just as reliably/securely."

...this has rarely proven to work. There's an old rule that you can't make high robustness systems by composing low-robustness components. They experience both individual and byzantine failures. That's why we see the companies building on them experiencing downtime that shouldn't happen on top of unavoidable downtime which I don't judge. So, certainly break the problem into smaller ones and compose simple (or cheap) solutions where possible. You just have a baseline of quality you need for the components. Commonly expressed as "weakest link" or "Garbage In, Garbage Out."

"I think the main reason there are less modern systems running for 15+ year timeframes is that the centralized models of yore only remain valid within traditional large organizations that are slow moving: finance, government infrastructure, military, etc."

Someone else speculated the same thing. There's some truth to it. Yet, there's overlap between the kinds of services running on them and in the modern, downtime-prone infrastructures. The stuff works on robust systems of old times but fails on new ones. What's the key difference? One was designed to be robust and one is a composition of pieces of known to unknown quality. Garbage in, garbage out.

"as COTS hardware + FOSS topple traditional mainframe vendors through cheap and highly scalable clustering."

They're definitely cheaper and faster. That's been the case since Beowulf clusters I built back in the day. Yet, their uptimes still haven't reached what OpenVMS hit in the 80's with bullet-proof clustering. Are you truly saying hardware and admin labor is so free right now that we can just throw dozens to hundreds of servers in 3-5 locations at every businesses' problems while ignoring the architectural, interface or code quality of any of it? I'll take QNX 2 here and 2 there over a bunch of Linux boxes any day so long as budget will allow the license. I'll have predictability, performance, self-healing, damage containment, and live updates all in a few megs of well-written code w/ POSIX apps.

See the difference between that and mainstream systems? Good architecture still matters. System/38 (AS/400), OpenVMS, NonStop, QNX, BeOS... all great architecture that squeezed way more out of any given piece of hardware, software, or admin effort. OpenVMS was also an example of medium assurance that was point of our discussion. Their Red/Blue iterations did 1 week development & test writing then 1 straight week of review and fixes with regression tests over weekends. Results were boxes so reliable admins sometimes forgot how to reboot it and such. Still not common on Windows and Linux boxes despite the great strides in reliability that nearly a billion dollars worth of labor bought those bad architectures. I like to poke at Linux folks that MINIX 3 eliminated most crashes in a few years with a small team while UNIX architecture took decades to mostly do the same thing. Architecture & assurance activities matter.

"though they are definitely capable, and with Linux it has been done"

I'd like to see evidence of that. The mainframes, AS/400's, VMS, NonStop's... these run all sorts of workloads without software repairs for years. Heavy workloads. I've investigated numerous claims of individual Linux boxes doing the same. It was almost always someone's barely-utilized, hobbyist web server, DHCP server, etc. I want to see the equivalent of a mainframe or VMS server running everything in a business 24/7 without a crash in years. Optionally that system getting lost due to never needing maintenance with people scouring the building looking for it. That was a recurring problem with pizza box servers and embedded cards running aforementioned OS's. ;)

"they do run in harsh environments with limited resources in hundreds of millions - nay - billions of instances, extremely reliably."

Again, a source for this. They certainly run regular workloads they're optimized for quite reliably. The cloud vendors optimizing on specific HW configurations with all kinds of disaster tolerance appear to run them reliably by hiding the failures. Yet, surveys of industry on their servers' downtime contradicts the overall claim with all kinds of downtime still in mainstream stuff. Plus, they show recent Windows servers ahead of Linux in reliability and AIX usually stayed on top. They don't include the stuff I mentioned due to maybe market share or perhaps the contrast would make the others look bad. ;)

Nonetheless, adopting medium assurance methods to build our components or using components built that way is a solution. It was proven... is used... in many commercial systems that have higher quality at acceptable price and performance. Outside one-offs, the only reason it's not happening is lack of knowledge or will to do it. Mainstream devs were told about the stuff for years so they just don't give a shit. Surprisingly, Microsoft is ahead in efforts as they implemented SDL, formal methods on drivers, integrity controls, app protections, safe language use, and so on. I would love to see that level of commitment on BSD and Linux side given I use both. Least they sometimes accept fixes from academics who apply various tools in their spare time or with grant funding. ;)