Formal methods have been used successfully for decades; it's not just a pipe dream. Perfect software should ideally be something like ultra-low-defect software,

Formal methods have been used successfully for decades; it's not just a pipe dream. Perfect software should ideally be something like ultra-low-defect software, though (that's the term the AdaCore folks use). There are also other projects that aim to make formal software development much easier [0][1] and of course there's SPARK Ada. [0] https://github.com/zetzit/zz https://github.com/zetzit/zz [1] https://github.com/dafny-lang/dafny https://github.com/dafny-lang/dafny