DARPA's High-Assurance Cyber Military Systems program is looking for a synthesizer capable of producing a machine-checkable proof that the generated code satisfies functional specifications as well as security and safety policies.

Verifying object code can mean the difference between success and failure, quality and crap. But skipping the step because a standard doesn’t require it or because it theoretically eats into profits is a surprisingly common practice. The author postulates that this practice is not only shortsighted but no longer valid.