3 ms·
About Cleanroom, the prohibition on unit testing is insane; CPU and compiler bug exists, so do subtleties in languages, and even good quality models in formaliz
by xorblurb 11y ago
About Cleanroom, the prohibition on unit testing is insane; CPU and compiler bug exists, so do subtleties in languages, and even good quality models in formalized forms have some defects that probably prevent to get a mathematical proof of correctness even if the CPU/Compiler would be defect free (ex: C++11 memory model - and I think the formal Java memory model also has some issues). They should do as if they are forbidden to do unit testing, but then once they are "sure" all their code is correct do it anyway. Having a separate team do some level of testing is fine, but there is value in also having some done by authors, because conveying all the intents and caveats and things taken into account when writing it but also things NOT done and the reason for that, about a piece of source code, even very small, is incredibly hard.
- nickpsecurity 11y agoOh I agree with you entirely. Not running code and no unit testing were critiques I had with it. I used it as an example of engineering software. Cleanroom certainly isnt the last word in that. Personally, as it's function-oriented, I'd combine it with a subset of Haskell that was easy to translate into imperative code. Build the app with Haskell, use QuickCheck/QuickSpec, test every execution path, covert channels via Flow Caml-like setup, and certified compilation to target with pre-verified runtime. Now, we can use that directly or use it as an executable spec for an imperative implementation. So, that's how I see applying Cleanroom today for most benefit. Maybe drop the statistical stuff, too.