I think people incorrectly assume that formal methods must be prohibitively expensive. Being able to incrementally work toward verification is what excites me about Ada 2012/SPARK. It’s not some pie in the sky theoretical thing anymore. It’s built in, so it’s another tool in my toolbox on the parts that need it and I can use the same annotations in the unverified parts of code to do checks during normal development.
I think people incorrectly assume that formal methods must be prohibitively expensive. Being able to incrementally work toward verification is what excites me about Ada 2012/SPARK. It’s not some pie in the sky theoretical thing anymore. It’s built in, so it’s another tool in my toolbox on the parts that need it and I can use the same annotations in the unverified parts of code to do checks during normal development.