There was some recent HN discussion on the limits of formal methods: https://news.ycombinator.com/item?id=12468479 https://news.ycombinator.com/item?id=1246847

There was some recent HN discussion on the limits of formal methods: https://news.ycombinator.com/item?id=12468479 https://news.ycombinator.com/item?id=12468479 If we're willing to accept broken software some of the time we can do far more, and in practice this is how the vast majority of software is developed. In this context I think "mathematical" vs "computational" has the colloquial meaning of "proven" vs "empirically tested".