Comment by peter_d_sherman

There also seems to be some intersection here between type-driven development and Proof Assistants:

https://en.wikipedia.org/wiki/Proof_assistant