@xahlee Dependent Typing with proposition-as-types and proofs-as-programs allows you to add formal specification and formal verification to code; Eg Idris, Coq, Agda.
@fabianhjr yes those are good.
but do they have documentation written as math text is written?
@xahlee depends if you are into Homotopy TT/Per Martin-Löf TT/Category Theory as foundations of mathematics.
@fabianhjr yes. am learning it.