In a way, writing types is proof-esque. It establishes some basic correctness guarantees regardless of the programming language. Some concepts like refinement types make it seem more "mathy", by requiring quantifiers within programs: https://ucsd-progsys.github.io/liquidhaskell/blogposts/2019-...

Someone without any background in the subject would probably find Dafny interesting.