When I was in college, lo so many years ago, one of my classes involved a book which was entitled The Science of Programming, and it showed how to program using a language in which one could prove that a program was "correct." This book is what introduced me to the concept of Formal Verification. At the time, and for many years afterwards, it was clear that development in this way would be confined to the classroom for the time being, because in the "real world" (so called) neither the economics of software development nor the proclivities of the majority of programmers lent themselves to spending the extra time needed to write software in the above manner.

A friend of mine recently sent me a link to this article from Quanta magazine. This article indicates that a language based on formal verification, called F*, is gaining some traction in the real world with respect to writing code which is provably immune from coding vulnerabilities which are often exploited by hackers. The next page will give a summary of the article contents.