4 ms·

> I think this is one of the big differences between junior and senior software developers. You can see juniors get very frustrated with bugs because the code t

> I think this is one of the big differences between junior and senior software developers. You can see juniors get very frustrated with bugs because the code they delivered was 'working'. Seniors realize that software only works within well defined parameters If that's the case, assuming those juniors have relevant degrees, they weren't paying attention in their lectures on testing. Any decent lecture series on software engineering in general, or on testing specifically, will cover that testing can almost never prove the absence of all bugs, as exhaustive testing is rarely practical. If you want proof of correctness, formal methods are the only game in town. I like your hierarchy, that's really a neat perspective on correctness, and the tongue can be returned to its preferred posture. Perhaps a fifth entry might be useful, along the lines of As Deployed, to cover bugs in the platform (the compiler, standard library, OS, and hardware). This might not perfectly align with Working As Implemented, unless the implementation is taken to include the platform.

rileymat2 6y ago
> If you want proof of correctness, formal methods are the only game in town. How does this take into account unknown parameters indicated in the parent? For instance, expecting little endian but getting big endian in a different environment?
- MaxBarraclough 6y ago
  With the disclaimer that I'm not an expert on formal methods, or on endianness: endianness is something that could be formally modelled, but it seems to me the better approach is to write code that's insensitive to platform endianness. Another approach might be to ensure such platform-specific assumptions hold true by using static assertions, so that the build will fail if the assumptions are not met. A third approach might be to write (and verify) separate code for different endiannesses. Any one of these approaches should make it possible to write formally verifiable C code that behaves identically regardless of endianness. Of course, by using a formal verification framework, you aren't worrying about being blindsided by something like endianness, you're worrying about getting the thing to verify. If it verifies, that means you haven't made any fiddly mistakes with concerns like endianness. The SPARK language (designed for formal verification) doesn't let you write endian-sensitive code in the first place, if I understand correctly. (SPARK is technically not a fully deterministic language but it's very close. [0][1]) I don't know if there are circumstances where you must write endian-sensitive code, but don't think there are. I can imagine an endian-sensitive solution might perform better (e.g. simply reinterpreting an array of bytes as an array of 32-bit unsigned integers). [0] https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/portability_issues.html#parenthesized-arithmetic-operations https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/... [1] https://docs.adacore.com/spark2014-docs/html/ug/en/usage_scenarios.html#benefits-of-using-spark-for-portability https://docs.adacore.com/spark2014-docs/html/ug/en/usage_sce...

rileymat2 6y ago

> If you want proof of correctness, formal methods are the only game in town. How does this take into account unknown parameters indicated in the parent? For instance, expecting little endian but getting big endian in a different environment?

MaxBarraclough 6y ago
With the disclaimer that I'm not an expert on formal methods, or on endianness: endianness is something that could be formally modelled, but it seems to me the better approach is to write code that's insensitive to platform endianness. Another approach might be to ensure such platform-specific assumptions hold true by using static assertions, so that the build will fail if the assumptions are not met. A third approach might be to write (and verify) separate code for different endiannesses. Any one of these approaches should make it possible to write formally verifiable C code that behaves identically regardless of endianness. Of course, by using a formal verification framework, you aren't worrying about being blindsided by something like endianness, you're worrying about getting the thing to verify. If it verifies, that means you haven't made any fiddly mistakes with concerns like endianness. The SPARK language (designed for formal verification) doesn't let you write endian-sensitive code in the first place, if I understand correctly. (SPARK is technically not a fully deterministic language but it's very close. [0][1]) I don't know if there are circumstances where you must write endian-sensitive code, but don't think there are. I can imagine an endian-sensitive solution might perform better (e.g. simply reinterpreting an array of bytes as an array of 32-bit unsigned integers). [0] https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/portability_issues.html#parenthesized-arithmetic-operations https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/... [1] https://docs.adacore.com/spark2014-docs/html/ug/en/usage_scenarios.html#benefits-of-using-spark-for-portability https://docs.adacore.com/spark2014-docs/html/ug/en/usage_sce...