Az egyik dolog, amit nagyon szeretek a progmaton a Simon-féle analízis kurzusban, az az, ahogyan gyakorlatilag a semmiből, vagyis a ZF-ből és a valós számok axiómáiból építkezünk, és ha néha ki is hagyunk egy-egy bizonyítást, akkor arra külön fel van hívva a figyelmünk. Ennek az a csodálatos eredménye, hogy még így a hatodik félév közepén is bármilyen bonyolult tétel bizonyítása esetén elvileg rekonstruálható a teljes út az axiómáktól.

A SICP, mint alant kifejtem, ugyanilyen előadássorozat illetve könyv, a programozásról. Én egy-két évvel ezelőtt először az előadással találkoztam, ma már nem tudom, miért hagytam abba akkoriban a 6. előadás környékén. Most viszont elémkerült a könyv is, nekiugrottam, és kiderült, hogy a lényeg pont a második felében van.

Az első három fejezet ugyanis bármelyik, hasonló témájú könyvben előfordulna: az absztrakció különböző, egymásra épülő vagy éppen ortogonális szintjei, mint pl. (magasabbrendű) függvények, adatok és műveleteik együttes kezelése (hadd ne mondjam típus), az imperatív megközelítés a maga értékadásos-mellékhatásos fekélyeivel, Haskell-szerű lazy evaluáció. Az összes illusztráció Scheme-ben, egy Lisp dialektusban íródott, valójában az első három fejezet éppen arról szól, ahogyan a fenti absztrakciós eszközök céljainak megvizsgálásával felépül a nyelv szemantikája.

Az érdekességek a negyedik fejezetben kezdődnek. Először, egyfajta baseline-ként bemutat egy Scheme-ben írt Scheme interpretert, ennek ugye Lispben eleve komoly hagyományai vannak (összehasonlíthatatlanul olvashatóbb a mai szemnek ugyanennek a cikknek a Paul Graham által felújított változata). Ezzel már sokkal valóságosabbá válnak az eddigi programok, hiszen bár a kígyó még a saját farkába harap, de már kezünkben van az axiómáknak az a véges halmaza, amikből a konkrét Scheme programok szemantikája levezethető.

Ezekután bemutatja a Scheme pár leágazását, és persze hogy itt válik érdekeltté az intencionális programozó. A Lispben ugye régóta kultúrája van annak, hogy a problémákat a hozzájuk illesztett nyelven oldjuk meg, és utána vagy írjuk meg ennek a nyelvnek az értelmezését, vagy ágyazzuk be a nyelvet a Lispbe. Így aztán a tipikus Lisp programozó a legritkább esetben programozik Lispben, sokkal gyakrabban mindenféle ad-hoc Lisp' meg Lisp'' nyelvekben. A negyedik fejezet ilyen Scheme' nyelveket mutat be a lazy evaluációhoz és a nemdeterminisztikus futási szemantikához (ez utóbbi egyébként valószínűleg közel áll ahhoz, ahogyan a kvantumszámítógépeket fogjuk magasszinten programozni); illetve egy interpretált constraint-nyelvet.

És végül az utolsó fejezet az, ami odavág. Nem azért, mintha nem láttunk volna még a bootstrap-probléma megoldására gépi kódban írt compilert, hanem azért, ahogyan kerekké teszi a könyvet. Itt jön be ugyanis a korábban említett párhuzam az anal-kurzussal. Bebizonyítjuk, hogy létezik rendezett teljestest: a valódi, fizikai számítógépeket leíró regisztergép-modellen az utolsó bitig egyértelművé válik minden maradék kérdésre a válasz, a bemutatott, gépi kódú Scheme interpreter és fordító pedig hirtelen megfoghatóvá tesz minden, a könvyben megelőző példát. Handwaving-nek nyoma sem marad. Ahogy az utolsó előtti előadáson Abelson mondja: az utolsó, legnagyobb varázslat, hogy kiírtjuk a rendszerből a mágiát.