Melyik az a programnyelv, melynél helyességbizonyítást kell adni?

Csak annyira emlékszek, hogy az eljárásoknál/függvényeknél meg kell adni, hogy a bemenetek milyen feltételeknek kell megfelelniük, és hogy ha megfelelnek, akkor a kimenete milyen feltételeknek fog megfelelni. Arra nem emlékszek, hogy ellenőrzi-e, hogy tényleg megfelel-e neki a kimenete, de valószínűleg igen. Nem tudom hogy imperatív vagy deklaratív programnyelv-e. Nyilván magasszintű, hiszen alacsonyszintűben (assemblyben) ilyen nincs. A Haskell tudom hogy helyességbizonyítás leírására is jó, de tudtommal ott nem kell a függvényekhez megadni hogy milyen feltételnek kell megfelelnie a bemenetének, és hogy ekkor a kimenete milyen feltételnek fog megfelelni. Prologban se. Köszi.