I keep dipping my toes into “dependent-types”, never going all the way. Came across this long and interesting post on various languages that take different approaches here, with different tradeoffs (either being more focussed on theorem proving, or being more like “regular” programming languages, etc.)
One of the items was a comparison of how leftpad would be written/verified in each of these, so even though I can’t read/understand these yet, bookmarking the for future reference.
Agda:
Idris:
Liquid Haskell: https://github.com/hwayne/lets-prove-leftpad/blob/master/liquidhaskell/LeftPad.hs