Originally Posted by
bsieker
That is possibly the worst suggestion so far.
Assembly code is almost impossible to analyse for correctness in any meaningful way. It is far better (and provably so) to write in a well-specified (i. e. not C) language, prove the source code correct (for which scalable and practical techniques exist today), or define and prove correct a finite state machine and have code generated from it. That still leaves one with a need to have reasonable confidence in the compiler, but in many cases the service history for the most-used language core, and, in some recent cases, formally verified compilers, take care of that.
Just because you have one hero programmer who claims to have done it "Right" in assembly does not help you in any way because you need to demonstrate that it does what it is supposed to do (reliability), and never does what it is not supposed to do (safety), and ideally also never fails (availabilitiy). And this cannot be demonstrated by testing alone to the extremely high requirements needed in aviation. Assembly and machine code are avoided like the plague in safety-critical programming, and rightly so. Where some parts require it, extreme care must be taken to get it right, and the amount must be kept to a minimum.
Besides, as threemiles has pointed out, the implementation is not the problem (as far as we can tell, it may be flawless), but the specification. "Working as specified" can also mean that it did the wrong thing.
Bernd
Almost all the major 'programming errors' I have seen have been perfectly implemented errors in understanding due to poor systems analysis/design. Coding these days rarely has errors as there are many tools that can be used to verify the code it will also validate correctly as the code does just want the designer erroneously asked it to do. This is the shortcoming in mathematical approaches and formal proofs they do not find these errors in understanding but they
do limit the avionics; it is one of the reasons FMCs are beasts of little brain as anything with any power is beyond formal proof.
.