In a way, writing types is proof-esque. It establishes some basic correctness guarantees regardless of the programming language. Some concepts like refinement t

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-10-20-why-types.lhs https://ucsd-progsys.github.io/liquidhaskell/blogposts/2019-... Someone without any background in the subject would probably find Dafny interesting.