A funkcionális nyelvekben a szemantikai korrektség bizonyítása, ált. egyszerűbb és kézenfekvőbb, adott esetben megfelelő típuskényszerek ellenőrzésével automatizálható.
Ha szemantikai követelmények ki lennének kényszerítve (persze minden módszertanba kerülhet hiba) akkor utána csak a realtime követelmények teljesítésésén kellene majréznom(tényleg erre van valamilyen formális proof rendszer?), és azon már nem hogy valaki kifelejt mondjuk egy banális mph -> kmph átváltást a kódban.