Would the point not stand if they had said ML or Prolog?
then add additional specifications to clarify ambiguity when observed
That's such a clean, almost clinical way to describe, "After the software has caused several billion dollars in trading losses, bankrupting the entire company." (https://en.wikipedia.org/wiki/Knight_Capital_Group#2012_stoc...) Imagine if software with large inherent risk was developed using formal
methods, and the massive remainder of software was developed using rapid
development methods.
Imagine if we could tell the difference between use-cases with large inherent risk and the massive remainder of use-cases and avoid using software designed for low-risk situations in high-risk applications.