Bez ohledu na to, kolik bílých labutí jsme pozorovali, není oprávněný názor, že všechny labutě jsou bílé.
Také jste si všimli, jak v programování řešíme stejné problémy jako řeší vědátoři? Jasně, nejde si toho nevšimnout. Ale i tak to tu napíšu.
Věda se dá dělat několika způsoby. První je intuitivní. Prostě něco pozoruji, z pozorování vyvodím nějaké závěry a těm věřím. Moc se nezatěžuji experimenty, spíš se snažím používat hlavu a z konkrétních pozorování dělat obecné závěry. Všechny labutě, které jsem kdy viděl byly bílé, takže je jasné, že jsou všechny labutě bílé.
Tuto metodu můžu výrazně vylepšit tím, že se spojím s ostatními, předvedu jim svoje výsledky a nechám je tam hledat chyby. To je obrovský krok vpřed. Ostatní můžou najít moje chyby v logice a napravit je. Dokonce mohli vidět i něco, co jsem já předtím neviděl. Třeba dokonce někdo viděl modrou labuť?
Třetí krok je, že se snažím dělat systematické pokusy, které mi o skutečnosti řeknou mnohem víc než nahodilá pozorování. Záměrně ten jev pozoruji v různých podmínkách a snažím se ho pochopit hlouběji. Fyzika s tímto přístupem začala před pár set lety, ostatní vědy se postupně přidávaly a těch pár zbývajících se na to už pomalu chystá.
Ale je tu ještě čtvrtý krok, který zatím udělalo jen pár oborů. Nesnaží se jenom dělat pokusy, které jejich hypotézy potvrdí. Dělají pokusy, které je mají vyvrátit. Záměrně se snaží najít si na své víře chyby, snaží se vymyslet pokus, který jejich teorii rozbije. Snaží se najít labuť jiné barvy. Čím víc takových pokusů udělají, tím je ta hypotéza pravděpodobnější (i když jistoty nikdy nedosáhnou).
Čím dál daný obor je v tomto žebříčku, tím jsou jeho předpovědi užitečnější. Věříte víc předpovědím fyziků nebo ekonomů? Tím nechci říci, že by obory, které se nedostaly tak daleko jako fyzika, byly nějak retardované. Z velké části je to tím, že je mnohem snazší tisíckrát pustit dělovou kouli z věže, než nasimulovat chování celého státu nebo dokonce planety. Ale ať už je příčina jakákoliv, obory které se s pokusy dostaly dál, mají mnohem přesnější předpovědi.
Stejné je to i s programováním. Máme intuitivní přístup. Napíši kus kódu, spustím ho a párkrát do něj kliknu. Moc nepátrám jestli funguje. Jde to zkompilovat, vypadá to, že to funguje, tak to asi funguje. Navíc jsem to napsal já, takže to určitě bude dobře.
Toto se dá vylepšit za pomoci review. Kód ukážu někomu jinému, a on mi tam určitě najde nějaké chyby. Nicméně je to podobné jako když si ekonomové navzájem píší recenze. Dokud se neudělá pokus, tak je to jen výplod fantazie. Ano, i když vám review dělá nejlepší expert ve firmě, o výsledné funkčnosti to má stejnou vypovídající hodnotu, jako když vám recenzi napíše nejlepší ekonom na světě.
Jediné co má vypovídající hodnotu jsou testy. Myslíte si, že vaše aplikace funguje tak jak má? Dokud to systematicky nevyzkoušíte, tak je to jen výplod vaší fantazie a zbožné přání. Důležité je to slovo systematicky. Musíte se zamyslet nad tím jaké podmínky ten test můžou ovlivňovat, a všechny je vyzkoušet, pěkně jednu po druhé. Nicméně tu stále hrozí to, že se budete snažit tu svoji hypotézu jen potvrdit. Budete pořád chodit k tomu samému rybníku a pořád tam uvidíte jenom bílé labutě. Budete pořád procházet jenom základní scénáře, zkoušet to co zkoušíte vždycky. I to je veliký pokrok oproti předchozím variantám, ale je tu velké riziko zaslepenosti.
Pokud se totiž vědomě nepokoušíte hypotézu vyvrátit, tak hrozí, že budete nepříjemná fakta ignorovat. Možná ne záměrně, ale náš mozek je tak stavěný. Co se mu nehodí, to jednoduše nevnímá. Je proto potřeba změnit způsob myšlení a snažit se aktivně naše hypotézy vyvracet. Věříte, že máte aplikaci dobře zabezpečenou? Dokud se do ní pravidelně a systematicky nepokoušíte prolomit, tak je to zase spíš jen zbožné přání než realita. Věříte, že váš systém utáhne tu zátěž jakou potřebujete? A zkusili jste si to vyvrátit?
Oproti vědcům máme tu výhodu, že je software obvykle snadno testovatelný. Dá se jednoduše nasimulovat skoro cokoliv potřebujete. Takže nemáte stejnou výmluvu jakou mají všichni ti klimatologové, psychologové nebo ekonomové. Vy pokusy dělat můžete.
Takže je jen na vás, jestli chcete mít stejnou spolehlivost jako ekonomové nebo jestli by se vám spíš líbilo mít stejně spolehlivé předpovědi jako fyzici. Záleží jen na volbě metody, kterou si vyberete.
Jako malé bonusové cvičení tu mám různé hypotézy, které pravděpodobně máte kolem vaší aplikace. Zkuste jim přiřadit body, podle toho jak moc systematicky ověřujete jejich správnost. Jeden bod je za intuitivní přístup, dva za to samé plus review, tři za systematické testy a čtyři za systematické negativní testy.
- K našim datům se nikdo nepovolaný nedostane.
- Naše aplikace má správnou architekturu.
- UI je přehledné a pro zákazníka snadno pochopitelné.
- Nemáme tam žádnou chybu.
- Naše aplikace utáhne zátěž jakou potřebujeme.
- Produkční konfigurace je správně.
- Když dám všechny komponenty dohromady, tak to bude fungovat.
- Když udělám změnu, tak bude všechno výše uvedené i nadále platit.
- Blikající nadpisy jsou nejlepší na světě.
- Stihneme to naimplementovat včas.
- Ten nový proces zvýší naší produktivitu.
Tak co, kolik máte čtyřek? Já moc ne. A kolik jedniček? Víc než je zdrávo co? Tak co s tím uděláme?
Zdroje: Problémy popperovské falsifikace
Jen bych dodal, že v případě softwaru lze v analogii k vědě jít ještě dále než k fyzice. Fyzika je totiž stále v podstatě empirická věda — snaží se nějakým rozumně zjednodušeným způsobem aproximovat a predikovat reálný svět, ale fyzici jsou smířeni s tím, že jejich fyzikální model světa nebude nikdy 100% přesný a úplný.
Software ale sám o sobě nepopisuje reálný svět. Na fundamentální úrovni není software nic jiného než mechanismus hledání odpovědi na nějakou sadu logických otázek či vyčíslení nějaké (extrémně složité) matematické funkce (samozřejmě, že ta konkrétní odpověď nebo hodnota musí mít nějakou relevanci pro reálný svět, jinak by ten software nebyl užitečný, ale o to teď nejde).
Čili software se spíš než fyzikálnímu modelu podobá modelu matematickému. Ten ze své podstaty je zcela abstraktní a je postaven jen na sadě axiomů a odvozovacích pravidel zvolených podle libosti. Proč o tom mluvím? V případě softwaru totiž lze získat ještě lepší záruky, že je správně (tj. v souladu se zvolenými axiomy; v praxi s nějakou specifikací toho, co má software dělat), než poskytují pozitivní či negativní testy. Je možné zkonstruovat matematický důkaz správnosti, který nevyvratitelně dokládá soulad implementace softwaru s jeho specifikací. Metody konstrukce takového důkazu navíc mohou zaručit, že objeví každý protipříklad, který zabraňuje důkaz zkonstruovat, a tak zaručeně najdou skutečně všechny chyby (tj. odchylky od specifikace).
To jsou nepoměrně silnější záruky než libovolně podrobné testování, protože testováním lze vždy pokrýt jen určitou (typicky malou) část celého potenciálního stavového prostoru softwaru (pokrývá-li nějaké testování skutečně celý potenciální stavový prostor, je to v podstatě exhaustivní způsob konstrukce matematického důkazu správnosti).
Je jasné, že všechny metody tzv. formální verifikace software (https://en.wikipedia.org/wiki/Formal_verification), ať už je to model checking, abstraktní interpretace, symbolická simulace atd., mají své praktické limity. Reálně je v dnešní době schůdné aplikovat je jen na rozumně malé a izolované části softwaru a své největší uplatnení najdou zatím stále jen v mission-critical a safety-critical aplikacích. Jejich masové nasazování pro “běžné” programování je zatím stále utopie. Nicméně první jarní vlaštovky se najdou, ať jde o verifikovaná mikrojádra operačních systémů nebo důkazy bezespornosti algoritmů TCP/IP stacku. Celkem snadno se dnes už dají verifikovat implementace pokročilých datových struktur nebo korektnost vícevláknového kódu na nepřítomnost deadlocku, race conditions atd. A pokud vás váš moderní překladač upozorňuje na používání neinicializovaných proměnných nebo nedosažitelný kód, je to taky malá formální verifikace vůči poměrně jednoduché formální specifikaci.
Myslím si, že dnešní programátoři by měli mít o metodách formální verifikace alespoň základní povědomí, stejně jako dnes už nemohou existovat bez povědomí o správných metodách testování. Minimálně pro případy, kdy chtějí mít naprostou (matematickou) jistotu, že jejich implementace B+ stromu je korektní nebo že jejich vícevláknový kód neobsahuje deadlock.
Mě se na matematice taky vždycky líbilo jak je elegantní a čistá. Čistá je ale jenom díky tomu, že se nešpiní s realitou. Software takový není. Software nakonec poběží na reálném hardware, na reálném operačním systému, bude používat reálné ovladače, překladač nebo virtuální stroj. Pokud chci dělat matematické dokazování, tak o všech těchto reálných a většinou neuvěřitelně složitých věcech musím udělat nějaké předpoklady. Co se ale stane, když ty předpoklady nebudou správně? Když se bude procesor chovat o maličko jinak, v OS bude chyba nebo virtuální stroj bude mít mezní případ, se kterým nepočítám? Pak můj důkaz bude k ničemu. Pokud to nebudu empiricky testovat, tak na to ani nepřijdu. Budu žít v iluzi toho, že je všechno v naprostém pořádku, protože mám neprůstřelný důkaz. Ekonomové také mají matematicky naprosto přesně dokázáno, jak se má ekonomika chovat. Důvod proč jim předpovědi nefungují není to, že nemají matematické důkazy. Důvod je to, že ty důkazy staví na předpokladech, které nejsou pravdivé.
Druhý důvod, proč se běžný programátor s formálním dokazováním nesetká je to, že běžní programátoři nepíší stromy nebo síťové protokoly. Běžní programátoři píší věci u kterých se zadání nedá popsat matematicky. Správnost svého kódu nemám jak dokazovat, protože nejpřesnější popis toho co má dělat je ten kód samotný. Testy mi alespoň dávají křížovou kontrolu.