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.