3 ms·
But when your deployment costs run into the 7 to 10 digit numbers, you might long for better peer review of your code. Formal proofs provide that.
by jlg23 5y ago
But when your deployment costs run into the 7 to 10 digit numbers, you might long for better peer review of your code. Formal proofs provide that.
- zozbot234 5y agoThe best application for formal proof is actually in lightweight sanity checks as opposed to "deep" review of your code. To put it very clearly, it should simply not be possible for a properly-engineered program to conflate feet w/ meters and crash a space probe as a direct result of that conflation. There's just no way that this is ever valid semantics.
- p_l 5y agointerestingly, that's one of the areas where Ada shines, as you can define your own integer subtype that will help you preserve the semantics (and Ada has, iirc, no implicit casts, so it would require explicit cast to push feet into metres (and it might be made so that such cast would actually convert the values properly)
- okl 5y agoAda subtypes are "compatible" in that you can implicitly convert them, you're referring to types.
- actinium226 5y ago> But when your deployment costs run into the 7 to 10 digit numbers That's when you throw things into simulation and do some Hardware-in-the-Loop testing. If I learned anything from studying the failure of Ariane V flight 1, it's that while analysis can be useful, testing is usually even better. https://en.wikipedia.org/wiki/Cluster_(spacecraft)#Launch_failure https://en.wikipedia.org/wiki/Cluster_(spacecraft)#Launch_fa...