Filozofia inżynierii: Edsger Dijkstra, elegancja nie jest opcjonalna

Najważniejsze wnioski

• Elegancja nie jest opcjonalna. Dla Dijkstry prostota jest warunkiem poprawności, a nie nagrodą odbieraną po jej osiągnięciu — nie da się udowodnić tego, czego nie sposób w pełni zrozumieć.
• Dowód bije testowanie. „Testowanie pokazuje obecność, a nie brak błędów”. Pewność co do poprawności płynie z rozumowania o programie, nigdy zaś z gromadzenia kolejnych zaliczonych testów.
• Myśl, zanim zaczniesz pisać kod. Swój algorytm najkrótszej ścieżki zaprojektował bez kartki i ołówka, zmuszając go do rozmiaru, który mieści się w jednej głowie — to ograniczenie zrodziło elegancję.
• Pisanie jest myśleniem. Rękopisy EWD, tworzone odręcznie wiecznym piórem, bez możliwości cofnięcia, sprawiały, że argument albo trzymał się w atramencie, albo upadał — tę samą dyscyplinę stosował do prozy.

Zasada

„Prostota jest warunkiem koniecznym niezawodności”. — Edsger W. Dijkstra, atrybucja (ok. 1975)¹

Zdanie to przetrwało jako jednowierszowy aforyzm, niemal notatka na marginesie, kojarzona z jego celowo prowokacyjnymi memorandami z około 1975 roku. Wyrwane z kontekstu brzmi jak slogan, lecz Dijkstra rozumiał je jako ścisłe twierdzenie logiczne. Niezawodności nie dodaje się do skomplikowanego systemu przez intensywniejsze testowanie. System, którego nie sposób w pełni zrozumieć, jest systemem, którego nie można udowodnić jako poprawnego, a system, którego poprawności nie da się udowodnić, zawiedzie w sposób, którego nikt nie przewidział. Prostota nie jest preferencją stylistyczną konkurującą z poprawnością. Jest tym, z czego poprawność się buduje. Nie sposób mieć drugiego bez pierwszego.

Odwraca to sposób, w jaki większość oprogramowania faktycznie powstaje. Powszechny odruch każe zbudować rzecz, doprowadzić ją do działania, a potem testować, aż błędy przestaną się ujawniać — traktując prostotę jako luksus, którym można się zająć później, jeśli starczy czasu. Cała kariera Dijkstry była argumentem, że ta kolejność jest odwrócona i niebezpieczna. Jego najczęściej cytowane zdanie to przestroga, która wynika z niej wprost: „Testowanie pokazuje obecność, a nie brak błędów”.² Zaliczony test nie mówi niczego o danych wejściowych, których nie wypróbowano. Jedynym sposobem, by wiedzieć, że program nie ma błędów, jest rozumowanie o nim — a rozumować można tylko o tym, co jest na tyle proste, by zmieścić się w jednej ludzkiej głowie. Elegancja, w ujęciu Dijkstry, „nie jest zbędnym luksusem, lecz czynnikiem, który często przesądza o sukcesie lub porażce”.³

To przekonanie umieszcza go u źródła całej tej serii. Tam, gdzie Linus Torvalds przekształca problem, aż przypadek szczególny znika, a John Carmack obdziera problem do jego szybkiego jądra, Dijkstra dostarczył leżącego u podstaw twierdzenia, które obaj odziedziczyli: eleganckie rozwiązanie i poprawne rozwiązanie to to samo rozwiązanie. To pierwotny argument za traktowaniem smaku jako systemu technicznego, a nie estetycznej zachcianki — i argument za dowodem ponad prawdopodobieństwem dekady przed tym, zanim ktokolwiek tak to nazwał.

Kontekst

Edsger Wybe Dijkstra urodził się 11 maja 1930 roku w Rotterdamie, w Holandii, a zmarł 6 sierpnia 2002 roku w Nuenen.⁴ Jego ojciec był chemikiem i prezesem Holenderskiego Towarzystwa Chemicznego; matka była matematyczką, która — według jego własnych słów — miała niezwykle jasne wyczucie tego, kiedy argument matematyczny jest elegancki, a kiedy jedynie działa. Studiował matematykę i fizykę teoretyczną w Lejdzie, po czym w 1952 roku podjął pracę programisty w Centrum Matematycznym w Amsterdamie — w momencie, gdy „programista” nie był jeszcze uznawanym zawodem. Gdy w 1957 roku próbował wpisać go jako swoje zajęcie na akcie ślubu, holenderskie władze podobno nie chciały tego przyjąć, ponieważ taki zawód oficjalnie nie istniał; musiał wpisać „fizyk teoretyczny”.⁴

Ten szczegół to nie ciekawostka. Dijkstra przez resztę życia obstawał, że programowanie jest rygorystyczną dyscypliną intelektualną, a nie rzemiosłem urzędniczym, i obstawanie to zaczęło się, zanim dyscyplina miała nazwę. Zajmował stanowisko w Centrum Matematycznym, następnie w 1962 roku został profesorem na Politechnice w Eindhoven, lata 70. spędził jako pracownik naukowy w Burroughs Corporation, a w 1984 roku objął Schlumberger Centennial Chair in Computer Sciences na Uniwersytecie Teksańskim w Austin, gdzie pozostał aż do przejścia na emeryturę w 1999 roku.⁴

W 1972 roku otrzymał Nagrodę Turinga ACM. Warto przeczytać uzasadnienie w całości, ponieważ nazywa ono tę zasadę lepiej niż jakiekolwiek streszczenie: „Za fundamentalny wkład w programowanie jako wzniosłe wyzwanie intelektualne; za elokwentne obstawanie i praktyczne wykazanie, że programy powinny być komponowane poprawnie, a nie jedynie debugowane do poprawności; za rozjaśniające postrzeganie problemów u podstaw projektowania programów”.⁵ Komponowane poprawnie, a nie jedynie debugowane do poprawności. Ta fraza to cały ten człowiek.

Dzieło

Algorytm najkrótszej ścieżki (1956, opublikowany 1959)

W 1956 roku poproszono Dijkstrę o znalezienie problemu, który zaprezentowałby możliwości nowego komputera ARMAC podczas jego oficjalnej inauguracji — czegoś, za czym mogłaby podążyć niefachowa publiczność. Wybrał najkrótszą trasę między dwoma spośród 64 holenderskich miast, ponieważ każdy mógł zrozumieć pytanie i sprawdzić odpowiedź. Rozwiązanie przyszło do niego w sposób, którego nigdy nie znudziło mu się opowiadać: „Pewnego ranka robiłem zakupy w Amsterdamie z moją młodą narzeczoną i zmęczeni usiedliśmy na tarasie kawiarni, by wypić filiżankę kawy, a ja właśnie zastanawiałem się, czy potrafię to zrobić, i wtedy zaprojektowałem algorytm najkrótszej ścieżki”.⁶ Zajęło to około dwudziestu minut.

Sposób, w jaki go znalazł, jest właśnie tą lekcją. „Jednym z powodów, dla których jest tak piękny” — powiedział później — „było to, że zaprojektowałem go bez kartki i ołówka. Później dowiedziałem się, że jedną z zalet projektowania bez kartki i ołówka jest to, że jest się niemal zmuszonym do unikania wszystkich możliwych do uniknięcia złożoności”.⁶ Nie mógł oprzeć się na brudnopisie, więc idea musiała być na tyle mała, by w całości zmieścić się w jego umyśle. Ograniczenie zrodziło elegancję. Nie publikował go przez trzy lata — artykuł z 1959 roku „A Note on Two Problems in Connexion with Graphs” w Numerische Mathematik liczy ledwie nieco ponad stronę — ponieważ, jak to ujął, programowanie nie było jeszcze uważane za zajęcie na tyle szacowne, by o nim pisać.⁶

Algorytm jest zachłanny: zawsze najpierw rozszerza najbliższy nieodwiedzony węzeł, jako rozszerzający się front fali, który po kolei dociera do każdego punktu w jego najkrótszej odległości. Jest na tyle prosty, by wyjaśnić go przy kawiarnianym stoliku, i jest dowodliwie optymalny — gdy front fali po raz pierwszy dotyka celu, tej ścieżki nie da się pobić. Prostota i poprawność nie stoją tu w napięciu. Są tym samym faktem.

„Go To Statement Considered Harmful” i programowanie strukturalne (1968)

W 1968 roku Dijkstra przesłał do Communications of the ACM list zatytułowany „A Case Against the Goto Statement”. Redaktor, Niklaus Wirth, zmienił tytuł na „Go To Statement Considered Harmful” — fraza ta zrodziła cały gatunek naśladownictw i jest dziś sławniejsza niż cokolwiek w samym liście.⁷ Argument Dijkstry nie był poradnikiem stylu. Był epistemologiczny. Nieograniczone goto pozwala sterowaniu przeskoczyć dokądkolwiek, co oznacza, że aby zrozumieć, co program robi w danym wierszu, trzeba czasem prześledzić każdą ścieżkę, która mogła do niego doprowadzić. Tekst programu i jego zachowanie rozchodzą się. Przy strukturalnym sterowaniu — sekwencji, wyborze i pętlach — tekst i wykonanie pozostają we wzajemnej zgodności, a o danym bloku można rozumować, czytając ten blok.

Argument jest tą samą zasadą co ograniczenie najkrótszej ścieżki, zastosowaną do projektowania języka: utrzymuj rzecz na tyle małą, by dało się o niej rozumować. Programowanie strukturalne nie polegało na zakazaniu słowa kluczowego. Chodziło o zachowanie ludzkiej zdolności do udowodnienia — przez lekturę — że program jest poprawny. Lista jego słownictwa przytoczona w uzasadnieniu Nagrody Turinga — „śmiertelny uścisk” (deadly embrace), „semafor”, „programowanie bez goto”, „programowanie strukturalne” — jest zapisem tego, jak gruntownie przekształcił język, w którym myślą programiści.⁵

Jego praca nad systemami operacyjnymi nosiła to samo DNA. System wieloprogramowy THE (1968) zbudowano jako ściśle warstwowe poziomy abstrakcji, z których każdy dawał się zweryfikować samodzielnie. Aby koordynować współbieżne procesy, wynalazł semafor oraz jego operacje P i V, a problem ucztujących filozofów (Dining Philosophers) ujął jako dydaktyczną destylację zakleszczenia i zagłodzenia — trudne pytanie o współbieżność uczynione na tyle małym, by zmieścić się w umyśle.⁴⁵ Później przyszła samostabilizacja, a w A Discipline of Programming (1976) — rachunek transformatorów predykatów / najsłabszego warunku wstępnego: metoda wyprowadzania programu i dowodu jego poprawności razem, ręka w rękę, zamiast pisania kodu i nadziei na jego późniejszą weryfikację.⁴⁵

Pokorny programista: dowód ponad testowanie (1972)

Wykład Dijkstry z okazji Nagrody Turinga, „The Humble Programmer” (EWD340), to najjaśniejsze sformułowanie tego, dlaczego prostota jest kwestią moralną, a nie jedynie praktyczną. Jego centralne twierdzenie dotyczy rozmiaru ludzkiego umysłu. „Kompetentny programista jest w pełni świadomy ściśle ograniczonego rozmiaru własnej czaszki; dlatego podchodzi do zadania programowania z pełną pokorą i, między innymi, unika sprytnych sztuczek jak ognia”.⁸ Spryt nie jest cnotą. Jest zakładem, że da się utrzymać w głowie więcej, niż jest się w stanie, a zakład ten rozstrzyga się na produkcji, na twoją niekorzyść.

Wykład wieńczy zalecenie, które brzmi jak akt założycielski oprogramowania poprawnego z założenia (correct-by-construction): „Wykonamy znacznie lepszą pracę programistyczną, pod warunkiem że podejdziemy do zadania z pełnym docenieniem jego ogromnej trudności, pod warunkiem że trzymać się będziemy skromnych i eleganckich języków programowania, pod warunkiem że uszanujemy wewnętrzne ograniczenia ludzkiego umysłu i podejdziemy do zadania jako Bardzo Pokorni Programiści”.⁸ Testowanie, w tym ujęciu, jest zasadniczo niewystarczające — nie dlatego, że jest bezużyteczne, lecz dlatego, że potrafi jedynie próbkować przestrzeń danych wejściowych. Kanoniczna, dłuższa forma jego przestrogi, z „Notes on Structured Programming”, jest jednoznaczna: „Testowanie programu może służyć do wykazania obecności błędów, lecz nigdy do wykazania ich braku!”⁹ Jeśli chcesz braku błędów, musisz to udowodnić, a udowodnić można jedynie to, co potrafisz zrozumieć.

Rękopisy EWD jako praktyka (lata 60.–2002)

Przez mniej więcej czterdzieści lat Dijkstra pisał ponumerowaną serię rękopisów — memorand, dowodów, sprawozdań z podróży, esejów i argumentów — opatrzonych jego inicjałami „EWD”. Seria sięga numeru EWD1318, obejmując ponad tysiąc rzeczywistych dokumentów; numery przewyższają liczbę dokumentów, ponieważ przypisywał numer, gdy zaczynał dany tekst, a nie każdy tekst został ukończony.⁴¹⁰ Większość powstała odręcznie, słynnie precyzyjnym pismem, wiecznym piórem. Nie szkicował na komputerze. Pisał rękopis, kopiował go i wysyłał pocztą do niewielkiego kręgu współpracowników, którzy go kopiowali i przekazywali dalej — przedinternetowy samizdat, który nadał EWD wpływ nieproporcjonalny do faktu, że niemal żaden nie został formalnie opublikowany.⁴¹⁰ Kompletna seria jest dziś zeskanowana i swobodnie dostępna w E.W. Dijkstra Archive na UT Austin.¹⁰

Praktyka była nieodłączna od filozofii. Pisanie ręcznie, powoli, bez możliwości cofnięcia, wymusza tę samą dyscyplinę co projektowanie bez kartki i ołówka: nie da się schować za objętością ani za poprawkami. Argument albo się trzyma, albo nie, a zobowiązujesz się do niego w atramencie. EWD pokazują, jak to wygląda, gdy inżynier traktuje samo pisanie jako narzędzie do jasnego myślenia, a jasność jako cały sens.

Metoda

Metodą jest jedno przekonanie stosowane nieustępliwie przez czterdzieści lat.

Uczyń to na tyle małym, by dało się o tym rozumować. Algorytm z kawiarni, strukturalny przepływ sterowania, warstwowy system THE, destylacja ucztujących filozofów — każde z nich jest aktem zmniejszania problemu, aż ludzki umysł zdoła objąć go w całości i sprawdzić. Złożoność, której nie potrafisz ogarnąć, jest złożonością, której nie możesz zaufać.

Dowodź, nie testuj. Testowanie próbkuje; dowód poświadcza. Rachunek transformatorów predykatów Dijkstry istnieje po to, by dowód i program były wyprowadzane razem, a nie po to, by jedno zostało napisane, a drugie doczepione. „Komponowane poprawnie, a nie jedynie debugowane do poprawności” to metoda w pięciu słowach.⁵

Traktuj elegancję jako dowód, nie ozdobę. Gdy rozwiązanie jest brzydkie, ta brzydota jest zwykle sygnałem, że problem nie został zrozumiany. Elegancja „przesądza o sukcesie lub porażce”, ponieważ elegancka forma to ta, która ma najmniej miejsc, w których może być błędna.³

Pisz, by myśleć. EWD nie były dokumentacją tworzoną po wykonaniu pracy. Były pracą — rozumowaniem uczynionym widzialnym, w medium, które karało machanie rękami. Projektowanie bez kartki i ołówka, a następnie powierzenie wyniku wiecznemu pióru, to ta sama dyscyplina dwa razy.

Łańcuch wpływów

Kto go ukształtował

Jego matka, matematyczka. Dijkstra przypisywał jej swoje wyczucie matematycznej elegancji — wyćwiczony instynkt co do tego, kiedy dowód jest nie tylko poprawny, lecz czysty. To rozróżnienie, między argumentem, który działa, a argumentem, który jest piękny, stało się osią całej jego kariery. (Wpływ formacyjny)

Przedsięwzięcie Algol 60. Dijkstra współbudował jeden z pierwszych kompilatorów Algol 60, a struktura blokowa i rekurencja tego języka dały mu surowiec dla programowania strukturalnego. Algol był dowodem, że język programowania można zaprojektować z myślą o jasności, zamiast pozwolić mu narosnąć w imię wygody. (Wpływ bezpośredni)

Matematyczna tradycja dowodu. Wykształcony jako matematyk i fizyk, zanim istniała „informatyka”, Dijkstra zaimportował standard dowodu w całości. Dla niego program był obiektem matematycznym, a pytanie nigdy nie brzmiało „czy wydaje się działać?”, lecz „czy potrafisz wykazać, że musi?”. (Wpływ formacyjny)

Kogo ukształtował

Każdego programistę, który pisze kod strukturalny. Zniknięcie goto z codziennego programowania, powszechność sekwencji/wyboru/iteracji oraz całe słownictwo współbieżności — semafory, zakleszczenie, wzajemne wykluczanie — to jego dziedzictwo działające niewidocznie w każdej bazie kodu napisanej od tamtej pory.

Metody formalne i weryfikacja programów. Rachunek transformatorów predykatów oraz ideał poprawności z założenia są bezpośrednimi przodkami współczesnej weryfikacji, sprawdzania modelowego (model checking) i kodu niosącego dowód (proof-carrying code). Obecne odrodzenie formalnie zweryfikowanego oprogramowania systemowego to argument Dijkstry, który nareszcie spotyka sprzęt dostatecznie szybki, by go uruchomić.

Autowizerunek dyscypliny. Bardziej niż jakikolwiek konkretny wytwór, Dijkstra ugruntował ideę, że programowanie jest gałęzią matematyki stosowanej zasługującą na rygor — a nie fachem, którego uczy się metodą prób i błędów. Sumienie tej dziedziny, na dobre i na złe, wciąż przemawia jego rytmem.

Nić przewodnia

Dijkstra jest źródłem, z którego wypływa reszta tej serii. „Dobry smak” Linusa Torvaldsa — przeróbka, w której przypadek szczególny znika — to prostota-jako-poprawność Dijkstry w idiomie hakera jądra: mniej gałęzi oznacza mniej miejsc, w których można się pomylić. Szybkie, proste jądro Johna Carmacka to to samo odejmowanie, wymierzone w sufit sprzętowy zamiast w dowód. A obstawanie Andreja Karpathy’ego przy przebudowywaniu systemu od zera, by naprawdę go zrozumieć, to „projektowanie bez kartki i ołówka” Dijkstry w kapeluszu głębokiego uczenia. Cała czwórka nie zgadza się niemal we wszystkim z wyjątkiem tej jednej rzeczy, która się liczy: elegancka struktura nie jest nakładana na poprawne rozwiązanie. Ona jest poprawnym rozwiązaniem. (Pomost serii)

Co z tego biorę

Zdaniem, do którego wracam, jest to odwrócenie: prostota jest warunkiem koniecznym niezawodności, a nie nagrodą, którą odbierasz po jej osiągnięciu. Większość wolnego, kruchego oprogramowania nie jest wolna i krucha dlatego, że ktoś pominął testowanie. Jest wolna i krucha dlatego, że nikt nigdy nie uczynił jej na tyle małą, by dało się ją zrozumieć, więc nikt nie potrafił o niej rozumować, a więc jedyną dostępną strategią jakości było testowanie, aż widoczne błędy ustały — co, jak powiedział Dijkstra, niczego nie poświadcza. To odwrócenie jest tym samym standardem co jakość będąca jedyną zmienną: pytanie nigdy nie brzmi „czy testy przeszły?”, lecz „czy rozumiem to na tyle dobrze, by wiedzieć, że jest poprawne?”.

W świecie, w którym teraz buduję — agentów AI, pętli narzędziowych, systemów generujących kod szybciej, niż jakikolwiek człowiek zdoła go przeczytać — przestroga Dijkstry jest ostrzejsza niż kiedykolwiek. Gdy agent pisze tysiąc wierszy, a testy świecą na zielono, jest to dokładnie ta sytuacja, którą opisał: obecność błędów nie została wykazana, a ich brak wykazać się nie da. Posunięcie Dijkstry polega na odmowie pozwolenia, by zrozumiałość kurczyła się w miarę, jak generowanie rośnie — na obstawaniu, by system pozostawał na tyle mały, na tyle warstwowy i na tyle czytelny, by ktoś wciąż mógł udowodnić jego poprawność. Ta dyscyplina jest powodem, dla którego traktuję warstwę weryfikacji jako nośną, nawet gdy żaden człowiek nie czyta kodu: testowanie pokazuje obecność, nie brak, a front fali zielonych ptaszków nie jest dowodem.

FAQ

Na czym polega filozofia inżynierii Edsgera Dijkstry?

Dijkstra utrzymywał, że prostota jest warunkiem koniecznym niezawodności: program musi być na tyle prosty, by człowiek mógł go w pełni zrozumieć, ponieważ tylko o zrozumiałym programie można rozumować i udowodnić jego poprawność. Twierdził, że programy powinny być „komponowane poprawnie, a nie jedynie debugowane do poprawności”, że testowanie może pokazać obecność błędów, lecz nigdy ich brak, oraz że elegancja nie jest ozdobą, ale „czynnikiem, który często przesądza o sukcesie lub porażce”. Spryt, w jego ujęciu, był wadą, ponieważ przekraczał ograniczoną pojemność ludzkiego umysłu.³⁵⁸⁹

Co wynalazł Edsger Dijkstra?

Dijkstra wynalazł algorytm najkrótszej ścieżki noszący jego imię (pomyślany w 1956, opublikowany w 1959), wprowadził semafor oraz operacje P/V do koordynacji współbieżnych procesów, zbudował warstwowy system wieloprogramowy THE, sformułował problem ucztujących filozofów, rozwinął programowanie strukturalne, zapoczątkował pojęcie samostabilizacji w systemach rozproszonych oraz opracował rachunek transformatorów predykatów / najsłabszego warunku wstępnego do wyprowadzania programów wraz z dowodami ich poprawności (w A Discipline of Programming, 1976). W 1972 roku otrzymał Nagrodę Turinga ACM.⁴⁵

Co oznacza zdanie „Testowanie pokazuje obecność, a nie brak błędów”?

Oznacza, że test może jedynie wykazać, iż błąd istnieje, wyzwalając go — nigdy nie zdoła wykazać, że żaden błąd nie istnieje, ponieważ żaden skończony zbiór testów nie pokrywa wszystkich możliwych danych wejściowych. Dijkstra wypowiedział je na konferencji NATO Software Engineering Conference w 1969 roku, a jego kanoniczną, dłuższą formę podał w „Notes on Structured Programming”: „Testowanie programu może służyć do wykazania obecności błędów, lecz nigdy do wykazania ich braku!”. Jego wniosek był taki, że pewność co do poprawności musi płynąć z dowodu i z projektowania programów na tyle prostych, by dało się o nich rozumować, a nie z gromadzenia zaliczonych testów.²⁹

Dlaczego Dijkstra pisał odręcznie i rozpowszechniał rękopisy EWD przez fotokopię?

EWD były serią ponad tysiąca ponumerowanych rękopisów, które Dijkstra pisał przez mniej więcej cztery dekady, w większości odręcznie wiecznym piórem, a następnie kopiował i wysyłał pocztą do niewielkiego kręgu, który je kopiował i przekazywał dalej. Pisanie powoli, ręcznie, bez klawisza cofania, wymuszało tę samą dyscyplinę co jego nawyk projektowania algorytmów bez kartki i ołówka: wymuszało jasność i karało machanie rękami, ponieważ argument zobowiązany atramentowi musiał naprawdę się trzymać. Kompletna seria jest zarchiwizowana i swobodnie dostępna na Uniwersytecie Teksańskim w Austin.⁶¹⁰

Źródła