Hardware design developed formal method for their logic ALUs and FPUs a long time ago. Although that clearly has it's limits. Especially timing.
The next frontier is for program proofs to stop being news and instead partial program proofs increasing program reliability to the point where any program updates except for features become news.
How we go from proofs of concept to useful proof tools is a question I don't yet see answers to.
Copyright © 2017, Eklektix, Inc.
Comments and public postings are copyrighted by their creators.
Linux is a registered trademark of Linus Torvalds