Voidaanko jotkut ohjelmointiongelmat ratkaista matematiikan avulla siten, että ne muunnetaan Curryn–Howardin vastaavuuden avulla matemaattisiksi todistuksiksi, jonka matemaatikko tai vaikka Coq tai Lean tarkistaa?
Joo kyllä näin on.
Aihe on jo aika vanha, joten et voi enää vastata siihen.