Tutto l'apparato di formalismi è utile per un po' di roba strettamente collegata al mondo matematico. Ad esempio le dimostrazioni di correttezza attraverso i dependet type. Fai qualche ricerca se ti va.