Originally Posted by
flash8
Many years ago in the 90's attended a course at Oxford Uni Computing Unit where we looked into the 747-400 FADEC SW development with (memory might fail me) SPARK Ada and formal verification, this dated from the mid to late 80's when Ada (and the SPARK subset) was pretty much in vogue and fitted the criteria as an extremely strongly-typed and strict Language. The work behind it was mind-blowing, and can only have improved since then, so software issues I expect to be quite rare, although never obviously impossible.