I am dont know so much about that field but I "feel" the same. It would be nice if someone who knows that stuff could reply here if this intuition is right or n

I am dont know so much about that field but I "feel" the same. It would be nice if someone who knows that stuff could reply here if this intuition is right or not. Eventually when we reason about our code "as standard" non-math programmers we are doing math & logic & proofs in our minds aren't we? And we capture the edge cases in forms of tests and hope for the best if we thought about and enumerated all the necessary ones. So eventually if - a language but more importantly - an ecosystem like that will get leverage, every existing ecosystem can slowly fade into that and develop further in this path. At the end (almost all) programmers are going to write proofs, because this is what works in scale. Please correct me if I am wrong!