I think it's probably also a programming-language thing. When I write in haskell, the sytnax of the language and construction of the abstraction hirarchy, with all the simpel and well-specified rules you have to follow, makes it easier to see what to proof and why. Also, with property based testing, it is essentially the substitution of proofs with anecdotal, empirical evidence. I feel like that if I would have the option, there are a lot of places where i would just naturally proof properties (I know about the practical difficulties of a lazy language...but I think they are a bit overstated. See richard eisenbergs thesis on dependent haskell).

I don't think this is obvious in python, at all. You are programming without thinking much about invariants and properties.