I mostly agree, but I think any new mathematical understanding will be an implicit one. For example, in Rust, although the underlying type system is affine, almost no one explicitly reasons about programs using affine logic