I'm familiar with dependently typed languages, I thought you might mean something different than semi-manual theorem proving. For instance, writing your program in a particular style that could maximally take advantage of automated SMT solving in LiquidHaskell or something.