@lupyuen
My initial expectation was: Oh, this is where #Ada and #SPARK will shine. But as the article explains in a few more words, garbage in, garbage out. If the requirements are insufficient for all use cases then a perfectly functioning software cannot prevent damage.

I wonder if there is a case though that the ability to automatically prove, rather than extensively test and then chase the 20th null pointer error also helps to focus on the correctness of the requirements ?