Když se dnes mluví o programovacích jazycích, debata obvykle míří k typům, výkonu, běhovému prostředí, ekosystému balíčků nebo množství opakovaného kódu. Vedle toho je tu starší otázka: musí program vždycky popisovat postup?

V imperativním jazyce většinou říkáte stroji, co má udělat krok za krokem. Načti data, projdi pole, ověř podmínku, zapiš výsledek. Logické a deklarativní jazyky začínají jinde. Popíšete fakta a pravidla, dotaz nebo omezení, a systém hledá odpověď. V ideálním případě zapisujete, co má platit, ne přesný sled kroků.

Prolog vznikl na začátku sedmdesátých let v Marseille, v době, kdy se logika, umělá inteligence a zpracování přirozeného jazyka potkávaly těsněji než dnes. Colmerauer a Roussel v textu The Birth of Prolog připomínají, že název Prolog byl v Marseille zvolen v roce 1972 jako zkratka z „programmation en logique“. Základní myšlenka byla jednoduchá: program může být sada faktů a pravidel. Výpočet začne dotazem.

Malý příklad vypadá takto:

parent(alice, bob).
parent(bob, clara).

ancestor(X, Y) :- parent(X, Y).
ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y).

?- ancestor(alice, Y).

Tady není explicitní cyklus přes graf, zásobník, fronta ani vlastní implementace prohledávání. Program pouze říká, co znamená být předkem. Prolog se pokusí najít hodnoty proměnné Y, pro které je dotaz pravdivý.

Právě kvůli tomu má smysl tuto oblast znát i dnes. Ne proto, že by vývojář měl přepsat backend do Prologu. Část problémů, které běžně řešíme ručně, jsou ve skutečnosti dotazy nad vztahy, pravidla nad stavem systému nebo omezení, která má splnit nějaký model. Pro takové úlohy často existuje vhodnější nástroj než další strom podmínek.

Ne jeden nový Prolog, ale několik modelů

Byla by chyba nazvat CodeQL, Rego, Z3 a Lean novými Prology. Každý stojí na jiném modelu: CodeQL a Datalog odvozují vztahy nad daty, Rego používá pravidla pro rozhodování, Z3 hledá model splňující zadaná omezení a Lean kontroluje důkaz.

Společná je jim deklarativní poloha. Autor popíše, co má platit, a specializované jádro dopočítá zbytek. Rozdíl je v tom, jaké otázky mu dáváme.

Prolog v běžných implementacích pracuje od cíle. Dostane dotaz, snaží se jej unifikovat s fakty a hlavami pravidel, vytváří rozhodovací body a při neúspěchu se vrací pomocí backtrackingu. Výukový text Learn Prolog Now! ukazuje právě tento model hledání důkazu: systém prochází znalostní bázi shora dolů, hledá unifikaci cíle s faktem nebo hlavou pravidla a zkouší další možnosti, když předchozí cesta neuspěje.

Datalog se historicky posunul směrem k databázím a relačnímu dotazování. V čisté podobě ubírá expresivitu, aby se dal lépe optimalizovat a vyhodnocovat zdola nahoru: od známých faktů se postupně odvozují další fakta, dokud systém nedojde k pevnému bodu. Soufflé popisuje Datalog jako deklarativní logický dotazovací jazyk pro rekurzivní dotazy a uvádí jeho použití v programové analýze, bezpečnosti, grafových databázích a deklarativním networkingu.

Když se ptáme, kam zmizelo logické programování, odpověď nezní „do jednoho nového jazyka“. Jeho části se usadily v nástrojích, které řeší užší problémy.

Datalog a CodeQL: kód jako databáze

Prolog se výborně vysvětluje. Datalog se dá snáz použít jako základ analyzéru.

Rozdíl je praktický. U Prologu se často musíte starat o to, jak vyhodnocovací jádro pravidla zkouší. Pořadí může rozhodnout, zda se výsledek najde rychle, pomalu, nebo zda se výpočet zacyklí. Datalog je omezenější, ale právě proto dobře sedí na analýzu velkých grafů vztahů. A zdrojový kód je po extrakci takový graf: funkce volají jiné funkce, proměnné nesou hodnoty, data tečou ze zdrojů do citlivých míst, typy a uzly AST tvoří relační strukturu.

Soufflé je čistý příklad tohoto přístupu. Dokumentace k překladu Soufflé popisuje, že nástroj ze specifikace v Datalogu generuje nativní paralelní C++ program. Vývojář tedy napíše pravidla analýzy a nástroj z nich vytvoří specializovaný analyzér.

Podobný posun je vidět u CodeQL. GitHub ho popisuje jako nástroj, který umožňuje dotazovat se na kód jako na data a hledat varianty zranitelnosti napříč kódovou základnou. CodeQL nejdřív vytvoří relační databázi kódu. Nad ní pak jazykové knihovny zpřístupňují reprezentace jako AST, control-flow a data-flow modely.

Samotný QL na první pohled nevypadá jako klasický Datalog. Má objektovější nadstavbu a knihovny pro konkrétní jazyky. Specifikace QL ale říká, že jde o dotazovací jazyk nad relačními daty a dialekt Datalogu se stratifikovanou sémantikou. Dokumentace k vyhodnocování QL programů popisuje bottom-up evaluaci a hledání nejmenšího pevného bodu.

To vysvětluje, proč je CodeQL silný u variant analysis. Pokud jednou popíšete tvar zranitelnosti jako vztah mezi zdrojem dat, cestou programem a nebezpečným použitím, systém může hledat další případy v tisících souborů. GitHub k tomu dokumentuje i multi-repository variant analysis, tedy běh dotazu přes vybranou množinu repozitářů.

V praxi tak přežívá část logického programování, jen ne jako univerzální jazyk pro psaní aplikací.

Rego: pravidla mimo aplikaci

Druhý dnešní domov deklarativního myšlení je policy-as-code. Tady nejde o analýzu zdrojového kódu, ale o rozhodování nad stavem systému: smí tento request projít, může se tento kontejner nasadit, odpovídá Terraform plan interním pravidlům, má uživatel právo provést akci nad konkrétním zdrojem?

Open Policy Agent k tomu používá jazyk Rego. Dokumentace OPA říká, že Rego je inspirované Datalogem a rozšiřuje jej pro práci se strukturovanými dokumenty typu JSON. Zároveň ho popisuje jako deklarativní jazyk, ve kterém se autor pravidel soustředí na to, co má dotaz vrátit, ne na přesný postup vyhodnocení.

Malá ukázka vystihuje tvar problému:

package auth

default allow := false

allow if {
  input.method == "GET"
  input.path == ["accounts", input.user]
}

Tady nejde o algoritmus ve stylu „nejdřív načti uživatele, pak projdi role, pak otestuj cestu“. Pravidlo říká, za jakých podmínek je rozhodnutí allow pravdivé. OPA dostane vstup, data a vrátí výsledek.

OPA má technický přínos hlavně v oddělení pravidel od služby, ne v tom, že by Rego bylo samo o sobě hezčí než podmínky v Go nebo Pythonu. Filozofie OPA stojí na tom, že politika se nemá zabetonovat do aplikační logiky. Má být čitelná, verzovatelná, testovatelná, distribuovatelná a spravovatelná zvlášť.

To je užitečné hlavně u infrastruktury a platforem. Kubernetes admission control, CI/CD pravidla, Terraform compliance, API gatewaye, Envoy nebo Istio: všude tam se opakuje stejný vzorec. Nějaký systém musí rychle rozhodnout nad konkrétním vstupem a sadou pravidel.

Limit je zřejmý. Rego není náhrada obecného programovacího jazyka. Jakmile v pravidlech začnete simulovat komplexní aplikační proces, čitelnost i výkon se zhorší. Dokumentace OPA má samostatnou část k výkonu politik a řeší tvar dat, indexované výrazy, iterace a partial evaluation. Deklarativní jazyk vás nezbaví potřeby rozumět tomu, co vyhodnocovací jádro dělá. Jen přesune problém z aplikačního kódu do samotných pravidel.

Z3: omezení, ne relační dotazy

Z3 se v této mapě snadno zařadí špatně. V běžném použití je to především SMT solver, ne dotazovací jazyk nad databází kódu jako CodeQL ani obecný jazyk pravidel typu Prolog. Zároveň má i fixedpoint/muZ část pro constrained Horn clauses a Datalog, takže hranice není úplně ostrá.

SMT, tedy satisfiability modulo theories, řeší splnitelnost logických formulí nad konkrétními teoriemi. Klasický SAT pracuje s booleovskými proměnnými. SMT přidává oblasti, které programátory zajímají častěji: celá čísla, reálná čísla, bit-vektory, pole, řetězce, datové typy nebo neinterpretované funkce. V textu Programming Z3 Nikolaj Bjørner popisuje Z3 jako SMT solver se specializovanými algoritmy pro background theories a spojuje SMT se software analysis, verification a symbolic execution.

Příklad v SMT-LIB vypadá jinak než Prolog:

(declare-const x Int)
(declare-const y Int)

(assert (>= x 0))
(assert (= y (+ x 1)))
(assert (> y 10))

(check-sat)
(get-model)

Otázka nezní „najdi předky Alice“. Otázka zní: existují hodnoty x a y, pro které všechna omezení platí? Pokud ano, solver může vrátit model. Pokud ne, vrátí unsat. U některých úloh ale solver nemusí splnitelnost rozhodnout a může vrátit i unknown, jak připomíná Z3 Guide u příkazu check-sat.

Z3 je silný, když potřebujete formulovat omezení, ověřovat vlastnosti, hledat modely, dělat symbolické vykonávání nebo program synthesis. Je slabší jako každodenní jazyk pravidel, která má číst celý tým. Malá změna v popisu problému může výrazně změnit výkon a u některých tříd formulí i to, zda solver vrátí rozhodný výsledek. Špatný model problému u solveru rychle vede k neprůhledným výsledkům.

Lean: důkaz místo dotazu

U Leanu má věta „jazyk má v sobě logiku“ ještě jiný význam. U Prologu se logika projevuje jako inference nad pravidly a dotazy. U Leanu je v type systému a v důkazním jádru.

Lean Language Reference říká, že Lean je interactive theorem prover založený na dependent type theory. Taktiky mohou s důkazem pomáhat, ale konečný důkaz znovu kontroluje malé jádro systému. Proto Lean nemá primárně odpovídat na dotaz nad daty, ale strojově ověřit, že tvrzení opravdu plyne z pravidel systému.

Práce s Leanem proto spočívá víc ve stavbě a údržbě důkazu než v dotazování nad daty. V CodeQL se ptáte: kde v kódu existuje podezřelý tok dat? V Rego se ptáte: je tento vstup povolený podle pravidel? V Z3 se ptáte: je tato sada omezení splnitelná? V Leanu dokazujete tvrzení v systému s přesněji vymezenou důvěryhodnou základnou.

Lean míří jinam než Prolog i běžné policy nástroje. Hodí se tam, kde chcete strojově kontrolovaný důkaz formální vlastnosti: matematický důkaz, ověřený algoritmus, formální model protokolu, návrh jazyka nebo část systému, u které nestačí testy a statická analýza. Cena je vysoká. Důkaz se musí napsat, udržovat a pochopit. Automatizace pomáhá, ale neudělá z formální verifikace běžný refactoring ticket.

Kde se to láme

Deklarativní zápis bývá často prezentován jako jednodušší. Platí to jen ve správné doméně.

Deklarativní nástroje vypadají jednoduše na prvních pěti řádcích. Skutečná náročnost přijde ve chvíli, kdy se pravidla rozrostou, výsledky je potřeba vysvětlit a výkon začne záviset na detailech vyhodnocování. U Prologu je to pořadí pravidel a backtracking, u Datalogu reprezentace světa, u Rega správa pravidel, u Z3 formulace omezení a u Leanu cena samotného důkazu.

Nejde o akademii bez praxe. Slabé místo je spíš ergonomie a přenos mentálního modelu do týmu. Jakmile má pravidla udržovat víc lidí, nestačí, že jsou deklarativní. Potřebují testy, review, vlastnictví a způsob, jak vysvětlit výsledek člověku, který pravidla nepsal.

Proto se z logického programování nestal hlavní styl psaní aplikací. Ze stejného důvodu ale přežilo jako specializovaný nástroj.

Kdy po čem sáhnout

Pro běžného vývojáře z toho neplyne povinnost učit se Prolog. Plyne z toho užitečná rozhodovací mapa.

Pokud řešíte bezpečnostní nebo sémantické dotazy nad zdrojovým kódem, začněte u CodeQL. Hodí se ve chvíli, kdy nechcete jen spustit hotový scanner, ale popsat vlastní vzor chyby a hledat jeho varianty.

Pokud řešíte pravidla nad requesty, deploymenty, Terraformem nebo Kubernetes objekty, patří do mapy OPA/Rego. Jeho hodnota není v eleganci syntaxe, ale v tom, že pravidla dostanou vlastní životní cyklus mimo aplikační kód.

Pokud řešíte omezení, modely, symbolické vykonávání nebo verifikaci, dává smysl Z3 nebo jiný SMT solver. Tady se vyplatí mít u návrhu člověka, který rozumí formálním metodám aspoň natolik, aby poznal špatně položenou otázku.

Pokud potřebujete formální důkaz, ne jen test, alert nebo model, začíná prostor pro Lean. Je to nejdražší cesta z této mapy, ale také jediná z uvedených možností, která míří ke strojově kontrolovanému důkazu vlastnosti.

A Prolog? Ten má pořád hodnotu. Ne nutně jako produkční jazyk pro nový systém, ale jako dobrá vstupní brána k pochopení myšlenky, že program nemusí být jen postup. Někdy může být program dotaz na vztahy. Někdy sada pravidel. Někdy omezení pro solver. A někdy důkaz.

Praktický závěr je prostý: kdykoli v aplikaci ručně udržujete rostoucí strom pravidel, kontrolujete vztahy v grafu nebo opisujete bezpečnostní invarianty do imperativního kódu, má smysl se zastavit. Možná nepotřebujete chytřejší if. Možná potřebujete jiný výpočetní model.