[dselsam]

Author here.

> Also as scribu states, this doesn't allow you to prove final goals of the system like "classify images with 95% accuracy", nor does it save you from insufficient or inaccurate data.

We focused on implementation-based notions of correctness, which are both much easier to state and much more useful when actually developing software, but in principle downstream notions of correctness could be stated and proved as well. For example, for some models and under some assumptions about the data, you could formally verify that the accuracy of your trained model will probably be high on an unseen test set. However, the limiting factor is that nobody knows that much yet about the assumptions under which most useful models (such as neural networks) are guaranteed to perform well.