🚀 go-pugleaf

In article <Pine.LNX.3.95.961125164856.1098A-100000@Qhara.qhara.waw.pl>, piotrek@jack.oeiizk.waw.pl (Piotr Walesiak) writes:

>Nie znam się dobrze na zagadnieniach bezpieczeństwa. Za to znam się trochę
>na inżynierii programowania i wiem, że nie ma sposobu ani siły, żeby
>stworzyć oprogramowanie o złożoności większej niż 1000 lini kodu od razu
>poprawne. Faktem jest natomiast, że w sytuacjach gdy oprogramowanie ma
>spełniać jakieś bardzo krytyczne funkcje, jest ono poddawane gruntownym
>testom regresyjnym (po wykryciu błędu jest on poprawiany i wszystkie testy
>zapuszczane są od początku i tak aż do momentu gdy produkt przejdzie
>wszystkie testy bezbłędnie). Błędy są bowiem rzeczą ludzką (a to ludzie
>tworzą oprogramowanie) i nikt nigdzie od nikogo nie wymaga pisania
>programów odrazu poprawnych.

Masz w 99.99% racje... Ten pozostaly 0.01% to te przypadki, kiedy pisze 
sie program na tyle nieskomplikowany i w na tyle sformalizowanym jezyku, 
ze mozna dostarczyc matematyczny dowod jego poprawnosci. Wtedy testowac
trzeba juz tylko hardware na ktorym to chodzi :-)

I, uprzedzajac okrzyki wzburzenia 'artystow programowania' - tak, znam
konkretne przypadki gdzie formalne metody dowodzenia poprawnosci programow
byly uzyte w tworzeniu komercyjnego oprogramowania. Nie wiem konkretnie ile 
mialy linii kodu, ale na pewno nie byly to programy trywialne.

JMP