It's relevant because such methods can be used to prove the absence of errors, a notable case is Ironsides, which is a formally proven DNS. (Their 2013 paper lists the things they were able to prove at around page 12; though the 2012 paper is a bit more explicit on how such were proven.)
The point is that we're now living in an age where we can prove properties of software in a cost-effective manner; essentially we've implemented [mathematical] theory (WRT programming) from 30 years ago, and it opens a whole new vista of software reliability.
Thank you for elaborating further.
I’ll look at the papers you recommended as well.