> I definitely wouldn't want to spend time proving correctness of every single line of code I write; it would make programming "no fun" zone and require rocket-science level of understanding.
Fortunately, you don't have to. Formal verification can be done as little or as much as you want (and personally, I find it's quite fun, but that's subjective).
You can look at it like it's testing on steroids - you can not only verify that some part of your code works for certain inputs, but you can verify that it works for all inputs! (for the definition of "work" that you decide to give it).
Yeah, it's fun to some extent; I still remember proving whole Peano arithmetic and then using that to prove functional programs. But doing real-world detail level I would probably go crazy fast; just making proofs some floating point computation does what it's supposed to would be extremely tricky due to bit-level stuff and stretching sparsity of representable numbers that could fit to xyz-bits of floating point.
Fortunately, you don't have to. Formal verification can be done as little or as much as you want (and personally, I find it's quite fun, but that's subjective).
You can look at it like it's testing on steroids - you can not only verify that some part of your code works for certain inputs, but you can verify that it works for all inputs! (for the definition of "work" that you decide to give it).