Igaz, cserébe valószínűleg sokkal biztonságosabb programok lennének, amelyek sokkal lassabban futnának, sokkal kevesebbet tudnának.
Olvass utána egy kicsit :) Van statikus és van dinamikus helyességbizonyítás. Az egyiknél fordítási időben ellenőrzi a dolgokat a program, a másiknál meg futási időben, ami nyilvánvalóan lassítja, ámde nem sokkal. Ma is szokás egy tesztelés alatt álló szoftverbe assert()-eket rakni, ámde az sem sokkal fogja vissza...
Arra kíváncsi vagyok, hogy egy repülőgép irányítását végző bizonyítottan helyes kód hogy lehet lassú, és hogyan lehet olyan programot írni rá, aminek nagyobb a funkcionalitása. Az utóbbi gondolom olyan lenne, hogy nem csak a hajtóművet vezérelné, hanem még kávét is főzne, nem? :(