Ostatnio omówiłem ogólne tło historyczne powojennej fascynacji potęgą rozumu. Dziś o tym, gdzie i jak fascynaci się mylili.
Każda, najfajniejsza nawet idea jest nic nie warta, jeżeli nie pasuje do realnie istniejącej rzeczywistości. W różnych dziedzinach ten reality check następuje w różnym czasie i w różnym nasileniu. Niektóre branże, na przykład filozofia (czy ogólnie nauki tzw. humanistyczne), mają znikomy styk z rzeczywistością, inne trochę większy, ale prawie zawsze da się ewentualne niezgodności wyprzeć jakimś "ale gdyby...". Jest jednak jedna branża w której od idei do jej brutalnej konfrontacji z rzeczywistością jest bardzo blisko - jest to informatyka. Przyjrzyjmy się więc informatyce omawianego okresu.
Realna - nie teoretyczna - informatyka, zaczęła się oczywiście od skonstruowania pierwszych, praktycznie działających komputerów. Najpierw programowano je czysto na wyczucie w kodzie maszynowym, później pojawiły się assemblery a potem pierwsze języki wysokiego poziomu jak Fortran czy Cobol. Syntaktyka tych języków została wymyślona zupełnie od czapy, jak tam się komuś wydawało że będzie dobrze. Wkrótce zaczęły się problemy z takimi odczapistycznymi definicjami - najbardziej znana jest historia błędu w programie fortranowym polegającego na tym, że ktoś zamiast przecinka w instrukcji pętli napisał kropkę. Skutek był taki, że sonda międzyplanetarna sterowana tym programem się rozwaliła. Zasadniczy problem polegał na tym, że języki programowania były zdefiniowane tylko opisowo w języku naturalnym, i każdy mógł interpretować taką definicję inaczej. I jak wtedy zapewnić, żeby ten sam program dawał te same wyniki skompilowany różnymi kompilatorami?
No i to było coś dla wyznawców rozumu - tym trzeba było się zająć naukowo. Zaczęto więc pracować nad dobrym definiowaniem języków programowania. Efektem tych starań był Algol 60. I trzeba przyznać, że to im się akurat udało. Algol 60 został zdefiniowany przy pomocy matematycznego formalizmu (notacji Backusa-Naura), pięknie i klarownie. Koncepcyjnie język ten nie różnił się znowu aż tak bardzo od obecnie używanych języków proceduralnych w rodzaju niegdysiejszego Pascala, C czy Javy (Javy bez obiektów oczywiście, obiekty to późniejsze koncepcje). W zasadzie jedynym istotnym błędem zrobionym przez projektantów tego języka było to, że nie pomyśleli o zdefiniowaniu instrukcji wejścia-wyjścia i każda implementacja miała inne. Ale ogólnie był to sukces idei.
Zachęceni sukcesem rozumowcy zajęli się następną ideą: Program zapisany jest przy pomocy matematycznego formalizmu. Całkiem jak na przykład twierdzenie matematyczne. Twierdzenie matematyczne dowodzimy, żeby sprawdzić czy jest poprawne. Dlaczego by nie zrobić tego samego z programem? Będziemy dowodzić poprawności programu tak samo jak twierdzenia i błędy w programach nie mają szans! No i oczywiście ten dowód ma zrobić automatycznie komputer!
Na pierwszy rzut oka idea była całkiem dobra. Pojawiło się mnóstwo prac i projektów na ten temat i nawet jakieś metody udało im się opracować. Ale teraz pytanie kontrolne dla czytelników zajmujących się programowaniem: Czy dowodzicie w sformalizowany sposób poprawności swoich programów? Jak sądzicie, dlaczego nie?
Ja wyjaśnię. Otóż ta koncepcja to totalne nieporozumienie. Dowiedzenie poprawności programu to wykazanie, że on robi dokładnie to, co ma robić. Skąd dowodzący poprawności komputer ma wiedzieć co program ma robić? Trzeba to zapisać w jakimś formalizmie. Łapiecie? Komputer ma porównać formalny zapis tego co program ma robić z formalnym zapisem tego jak program to robi. Czyli raz zapisujemy rozwiązanie problemu w formalizmie "celowym" a drugi raz w "implementacyjnym". No ale tak w zasadzie to jeżeli komputer potrafi porównać jeden formalizm z drugim, to chyba powinno się dać przekształcić jeden w drugi, czyż nie? Czyli ten nasz formalizm "celowy" to w zasadzie język jeszcze wyższego poziomu niż ten "implementacyjny". To tak właściwie na cholerę mamy pisać to samo dwa razy? Nie lepiej napisać raz, w tym języku wyższego poziomu, ale za to dobrze?
No ale załóżmy, że w jednym formalizmie napisze jeden człowiek, a w drugim drugi. Zawsze będzie to jakaś kontrola, co nie? To prawda. ale czy nie taniej i prościej będzie po prostu zrobić code review? I tak się bez niego nie obejdzie, jak chcemy robić porządnie.
Jest jeszcze drugi zarzut, o wiele poważniejszy. Przez takie formalne dowodzenie porównujemy nic więcej niż tylko dwie wersje rojeń na temat działania programu. Jeżeli obie wersje stworzy jeden człowiek, to nasze dowodzenie udowodni najwyżej, że jego rojenia są spójne. Przy dwóch różnych autorach będzie to dowód na spójność rojeń dwóch ludzi. Ale to nie jest wiele warte - tak naprawdę interesuje nas nie zgodność programu z rojeniami człowieka, tylko zgodność programu z rzeczywistością! Jeżeli programista będzie przekonany że jego program dostaje do obróbki znaki kodowane w ASCII to ŻADNE dowodzenie nie wykryje że program jest bez sensu, bo dane są w EBCDIC. Świat zewnętrzny, you fool!
I tak mniej więcej to się skończyło - pamiętam z jakiejś książki przykład udowodnionego i opublikowanego jako programu na 15 linii, w którym przez ręczną analizę znaleziono 10 błędów. Jeszcze później prace matematyków wykazały, że na przykład rozstrzygnięcie czy pętla w programie się kiedyś skończy, czy nie, jest w ogólnym wypadku niemożliwe. Czyli to i tak nic nie da.
Oczywiście zgadzam się, że używamy dziś narzędzi sprawdzających to czy tamto w programach, ale z formalnym dowodzeniem nie ma to nic wspólnego.
I jeszcze: Nawet gdyby takie dowodzenie działało, to nadawałoby się tylko do niektórych, dobrze zdefiniowanych kawałków, na przykład do sortowania tabeli czy innych zadań algorytmicznych. Ale typowy, realnie istniejący program, to jest taki wielki, wielopoziomowy switch (ewentualnie schowany pod postacią hierarchii klas) wewnątrz pętli nieskończonej, jak i czego tu dowodzić?
No ale tymczasem rozumowcy zajmowali się dalszym doskonaleniem na drodze do ultymatywnego zapanowania nad przyrodą. Teraz miała powstać nowa wersja Algolu, tym razem idealna, uniwersalna i ultymatywna (serio zapewniali, że nic innego nie będzie już potrzeba!). Wytoczono najcięższe armaty: do definicji formalnej van Wijngaarden opracował gramatykę dwupoziomową, która dawała możliwość ślicznego i ścisłego opisania języka. Twórcy Raportu języka uważali że jest on tak piękny i skończony, że zostało tylko wycyzelowanie ozdobników. Każdy rozdział raportu ozdobiono pasującym cytatem z literatury, zadbano nawet o reguły ozdabiania rozdziałów przy tłumaczeniu ich na inne języki naturalne. Język nazwano Algol 68 i był to chyba jedyny język programowania który najpierw w 100% zdefiniowano formalnie, a dopiero potem przystąpiono do jakichkolwiek prób implementacji kompilatora. No i tu zaczęły się problemy. Jak już pisałem - świat rzeczywisty, you fool!
- Raport był słabo zrozumiały, bo użyta notacja nie była prosta. Aż trzeba było opracować całkiem nową, bardziej zrozumiałą jego wersję, zwaną Revised Report, potrwało aż do 1973. Przy okazji wywalono z języka parę konstrukcji jako zbędnych i przekombinowanych.
- Revised Report miał 280 stron tekstu i to tylko na formalizm plus krótkie komentarze. Przecież czegoś takiego nikt nie ogarnie! Dla porównania raport Algolu 60 miał stron ze czterdzieści włącznie ze skorowidzem, przeciętny, ogarnialny język daje się zamknąć w dwudziestu-trzydziestu.
- Raport definiował na przykład że słowa kluczowe mogą być w różne w różnych językach naturalnych. Każdy, kto używał formuł w różnych wersjach językowych MS Office z pewnością znajdzie dla tego pomysłu kilka prostych, żołnierskich słów.
- Parser Algolu 68 okazał się niespodziewanie trudny do napisania. Ludzie próbowali, próbowali, ale udawało im się parsować tylko podzbiory konstrukcji języka. A przecież definicja formalna była taka piękna!
Wkrótce sprawa rypła się całkiem. Ktoś udowodnił, że gramatyki van Wijngaardena są nierozstrzygalne, czyli że napisanie kompletnego parsera tak zdefiniowanego języka jest niemożliwe. No i to był cios w sam fundament projektu, który przecież miał być wspaniałym, ostatecznym i nieskazitelnym pomnikiem ludzkiego geniuszu. A okazał się być pomnikiem arogancji i zadufania.
Historia Algolu 68 jest typowa dla tamtych czasów i podobne znajdziemy również w innych branżach. Nimi zajmiemy się w jednej z następnych notek.
Podobno w czasie, gdy rozważano zastąpieniu Algolu-60 czymś nowszym na stole leżały dwie propozycje: Algol-68 i to, co dzisiaj znamy jako Pascal.
Komisja wybrała wspanialszy projekt…
BTW czytałem kiedyś artykuł (nieguglalny) o Pięknej Lady Algol, której urodę mimo wieku, widać do dziś.
Miała mnóstwo dzieci, jedno nawet z Fortranem (PL/I oczywiście…)
@pascal
Anegdota ładna, ale zdecydowanie nieprawdziwa. Dokładnie wiadomo kiedy i jak powstał Pascal, a było to dopiero w 1971. I wtedy nie było jeszcze żadnego kompilatora, bo była to tylko taka prosta, Algolo(60)podobna notacja do użytku na wykładach.
A jednak. Oczywiście na stole leżał nie Pascal, ale Algol X opracowany m.in. przez Wirtha.
Na podstawie doświadczeń przy tworzeniu Algolu X powstał Pascal.
Bardzo ciekawy cykl
@kontakt z rzeczywistością
Przypomniał mi się dowcip jaki opowiadali fizycy teoretycy (kiedyś pracowałem z) o filozofach: Jakie są trzy podstawowe narzędzia fizyka teoretyka? Kartka, długopis i kosz na śmieci. A narzędzia filozofa? To samo, tylko nie potrzeba kosza.
@dane wejściowe
wszystkim przyszłym programistom wkłada się do głowy (a przynajmniej powinno) pojęcie walidacji danych wejściowych. Ze względu na wszystkie przepełnienia bufora czy sql-injection. Ciekawe czy spece od Algola mieli taki problem.
@sql-injection
Szybki gugiel pokazuje, że pierwsza publiczna dyskusja o SQL-injection była w roku 1998. Więc 30 lat wcześniej problem był raczej nieznany lub bardzo niszowy.
Miałem kiedyś jakąś starą książkę, w której omawiali różne techniki wyciągania z bazy danych rzeczy, których nie powinno dać się wyciągnąć (i jak się przed tym zabezpieczyć). Chciałem teraz poszukać czy było tam coś w stylu SQL-injection tylko bez tej nazwy, ale wygląda że już dawno mi zaginęła. Albo może i nie, ale nie kojarzę która to była z tych co stoją na półce.
Akurat nie chodziło mi konkretnie o sql-iniection, tylko o to, że pod wpływem danych wejściowych pracujący dotąd całkiem dobrze program może zacząć robić coś całkiem innego (zwykle mocno niepożądanego) niż spodziewał się jego twórca. I że nie wiem, czy założenia że program nie zrobi czegoś takiego da się w jakiś ogólny sposób dowodzić. I jak długo taki dowód będzie ważny.
@dowodzenie
Oczywiście że się nie da. Całe to dowodzenie to było teoretyzowanie dla niektórych, bardzo specyficznych przypadków o minimalnym znaczeniu praktycznym. Ale było to w modzie i granty (czy jaki był wtedy system finansowania) dało się na to wyciągnąć.