Smukke programmer?

Mit program til primalitetstest

I dag underviste jeg i kurset “Programmeringsparadigmer” på kandidatuddannelserne i datalogi og software. (Der var kun lidt under halvdelen af holdet på 90 studerende til stede; det ser ud til at være et vilkår nu, at mange bliver væk, men det er en anden snak.)

Denne eftermiddag tog vi fat i programmering i Haskell, der er et af mine yndlingsprogrammeringssprog, bl.a. fordi det er baseret så pænt på den typede lambda-kalkyle, som jeg holder meget af, og på sædvanlig matematisk notation. Jeg har til gengæld aldrig været så glad for de C-agtige programmeringssprog, som de studerende lærer at programmere fra første studieår og frem (og ja, jeg ved at det er en idiosynkrasi at have det sådan).

En af opgaverne gik ud på at lave en lille Haskell-funktion, der kan finde ud af om et naturligt tal er et primtal. Man kan skrive programmet på to linjer, og mange af de løsninger, vi så, lykkedes med det. På et tidspunkt sagde jeg (det var vist lige lovligt hoverende): Nå, det kan man nok ikke skrive på to linjer i et C-agtigt programmeringssprog! Jeg måtte trække i land – for det kan man jo godt. Linjerne skal bare være meget, meget lange.

Der var i det hele taget mange pæne løsninger fra de studerende i dag. Nogle steder undervejs så jeg nu også nogle underlige “knaster” i ellers pæne programmer, og dem bemærker jeg derfor endnu mere. Et typisk eksempel på en “knast” opstår, når man vil finde ud af om værdierne af variablerne p og q er ens. Mange skriver

if p = q then True else False

Dette udtryk er underligt at se, for det er sandt hvis og kun hvis p er lig med q. Det er nok at skrive p = q, men mange opdager det ikke – formodentlig fordi de først har lært programmeringssprog, hvor logiske udsagn ikke er “førsteklasses”.

Og alt dette får mig til at tænke på, at der jo er en form for æstetik i programmeringssammenhænge, præcis som der er i matematik, og at det er en æstetik, som vi nok ikke underviser i, men gerne vil fremme. Vi vil gerne kunne forklare, hvorfor det lille eksempel ovenfor er en “knast”.

Der er blevet tænkt over det af og til, men der er ikke rigtig nogen “datalogiens æstetik”, ligesom der heller ikke er en “matematisk æstetik”: Vi har ofte en vag fornemmelse af at “dette er pænt”.

Robin Hill, der er filosof og ansat ved University of Wyoming, men faktisk også har en baggrund i matematisk logik og i datalogi (hun har en Ph.D i datalogi) skrev sidste år en interessant lille klumme om hvornår programmer er elegante.

Hun fremhæver fire kriterier: (1) minimalitet, (2) at udrette det, det skal  (hun bruger ordet “accomplishment” her, men der er ikke nogen god oversættelse her) (3) beskedenhed (ikke at gøre uskøn brug af særligt snedige tricks), og (4) ny indsigt (hun bruger ordet “revelation” på engelsk, men “åbenbaring” lyder så underligt religiøst). Det er f.eks. ikke nok, at et program er kort – korte programmer kan være meget grimme og indforståede.

Det er et rigtig interessant bud, for præcis de samme kriterier kan man nemlig give for beviser i matematik. En skæg bog (synes jeg!) er bogen Proofs from THE BOOK, der er en samling af ekstra elegante beviser for grundlæggende resultater i matematik, og den gør brug af nogle meget tilsvarende kriterier.  Bogens titel henviser til den ikke helt ukendte ungarske matematiker Paul Erdös, der hævdede at Gud havde en bog i himlen, der rummede alle de mest elegante beviser for matematiske sætninger!

Og som en lille krølle vil jeg bemærke, at det måske ikke er så sært, hvis kriterierne er de samme. For et program i Haskell er jo faktisk også et bevis i typeteoretisk forstand: En type i Haskell er nemlig en logisk formel i intuitionistisk prædikatlogik, og et udtryk med denne type er i helt præcis forstand et bevis for denne formel.

(Visited 50 times, 1 visits today)
Loading Facebook Comments ...

Skriv et svar