Prawo, lewo, zasada, kwas

Na tym najlepszym ze światów jest wiele rzeczy niepewnych, nie sprawdzonych, niejasnych. Szczególnie w nauce bywa się ostrożnym, czasami aż do przesady. Mówimy więc o trzech zasadach Newtona, o prawie Archimedesa, ale pomimo upływu ponad stu lat i setek udanych eksperymentów, ciągle jeszcze mamy Teorię Względności. A przecież powinno być Prawo Einsteina albo Zasada Względności.

Na tym najlepszym ze światów jest wiele rzeczy niepewnych, nie sprawdzonych, niejasnych. Szczególnie w nauce bywa się ostrożnym, czasami aż do przesady. Mówimy więc o trzech zasadach Newtona, o prawie Archimedesa, ale pomimo upływu ponad stu lat i setek udanych eksperymentów, ciągle jeszcze mamy Teorię Względności. A przecież powinno być Prawo Einsteina albo Zasada Względności.

W matematyce, jako nauce oderwanej od rzeczywistości, są tylko twierdzenia udowodnione, jak Twierdzenie Pitagorasa, albo też nie, jak np. postulat Golbacha (przypominam: każda liczba parzysta większa niż dwa podobno da się wyrazić jako suma dwu liczb pierwszych).

Styk matematyki z realnością życia codziennego jest najtrudniejszy. Pewne twierdzenia matematyczne z góry jednak skazują nas na porażkę, nawet w zawężonych ramach modelu rzeczywistości. Wśród nich najbardziej ponure jest Twierdzenie Goedla. Pisałem już o nim rok temu w felietonie XX, czyli dywergencja, uważając, że można nie wiedzieć, kto to Szekspir, ale musi się znać implikacje pracy Kurta Goedla. Dla zajmujących się zawodowo informatyką wniosek zeń jest prosty: nie można udowodnić poprawności wszystkich programów. Koniec i kropka. Po prostu nie da się.

Wydawałoby się, że prawdę tę znają od kołyski wszyscy Czytelnicy naszego czasopisma. O autorach nie wspominam, bo to powinno być dla nich oczywiste. Tymczasem jakiś czas temu mój sąsiad pisujący na tych samych stronach pozwolił sobie na taką oto uwagę: "Doskonale wiemy, jak trudno udowodnić, że napisany program jest poprawny. O ile w przypadku niewielkich programików jest to względnie proste, o tyle staje się prawie niemożliwe w przypadku dużych systemów". (Włodzimierz Serwiński Bajki i hipotezy CW 42/2001). Nie wiem, ilu Czytelników CW przesłało listy protestacyjne, pewnie nikt, bo i po co? Przecież to takie oczywiste.

Zdecydowałem się napisać ten tekst, bo myślę, że nie można pozostawić sprawy bez komentarza. Rozumiem, że jak się pojechało do Nazca w Peru, to człowiek widzi potem wszystko inaczej. Niestety, twierdzenie pana G. działa pod każdą szerokością geograficzną i niezależnie od tego, czy weń wierzymy, czy też nie. To nie są religie, z których każda ma swego "prawdziwego" Boga, ani też jedynie słuszna doktryna, pozwalająca uszczęśliwić sfrustrowaną część ludzkości. To jest udowodnione twierdzenie. Traf chciał, że znajdujące wprost zastosowanie w teorii programowania.

Żadne słowa nie zmienią konsekwencji Twierdzenia Goedla, nawet jeśli powtórzymy tysiąc razy, że to tylko matematyka, a nie rzeczywistość. Nie można od nikogo oczekiwać, że przy odrobinie staranności i testowania stworzy pewny, poprawny program. Bowiem program ten będzie wykonywany pod niepewnym systemem operacyjnym, kompilowany przez niesprawdzalny kompilator i testowany przez nie znany program, czyli nasz mózg. Mówiąc krótko - zawsze będą istniały programy, o poprawności których nie da się powiedzieć nic dobrego, a programów takich będzie nieskończenie wiele. Wśród nich zapewne i nasze dzieła. Co nie oznacza, że zachęcam Czytelników do pisania złych programów.

Proszę tylko nigdy nikomu nie dawać gwarancji, że coś jest poprawne.

Nigdy!

W celu komercyjnej reprodukcji treści Computerworld należy zakupić licencję. Skontaktuj się z naszym partnerem, YGS Group, pod adresem [email protected]

TOP 200