Om grymheten i att verkligen lära ut datavetenskap

"On the Cruelty of Really Teaching Computing Science" är en vetenskaplig artikel från 1988 av EW Dijkstra som hävdar att datorprogrammering bör förstås som en gren av matematiken och att ett programs formella bevisbarhet är ett viktigt kriterium för korrekthet.

Trots titeln handlar det mesta av artikeln om Dijkstras försök att sätta in datavetenskap i ett bredare perspektiv inom naturvetenskap , och undervisningen tas upp som en följd i slutet. Dijkstra gjorde specifikt ett "förslag till en introduktionsprogrammeringskurs för förstaårsstudenter" som bestod av Hoare-logik som ett otolkat formellt system .

Debatt om genomförbarhet

Sedan termen "programvaruteknik" myntades har formell verifiering nästan alltid ansetts vara för resurskrävande för att vara genomförbar. I komplexa applikationer är svårigheten att korrekt specificera vad programmet ska göra i första hand också en vanlig felkälla. Andra metoder för mjukvarutestning används i allmänhet för att försöka eliminera buggar och många andra faktorer beaktas vid mätningen av mjukvarans kvalitet .

Fram till slutet av sitt liv hävdade Dijkstra att de centrala utmaningarna med datoranvändning inte hade möts på ett tillfredsställande sätt, på grund av en otillräcklig betoning på programmets korrekthet (även om det inte undanröjde andra krav, såsom underhållbarhet och effektivitet ).

Pedagogiskt arv

Datavetenskap som lärs ut idag följer inte alla Dijkstras råd. Läroplanerna betonar generellt tekniker för att hantera komplexitet och förbereda sig för framtida förändringar, efter Dijkstras tidigare skrifter. Dessa inkluderar abstraktion , programmering genom kontrakt och designmönster . Programmeringstekniker för att undvika buggar och konventionella programvarutestmetoder lärs ut som grundläggande krav, och eleverna utsätts för vissa matematiska verktyg, men formella verifieringsmetoder ingår inte i läroplanen förutom kanske som ett avancerat ämne. Så på något sätt har Dijkstras idéer följts; de idéer han kände starkast för har dock inte varit det.

Nybildade läroplaner i programvaruteknik har antagit Dijkstras rekommendationer. Fokus för dessa program är den formella specifikationen av mjukvarukrav och design för att underlätta den formella valideringen av systemets korrekthet. I Kanada är de ofta ackrediterade ingenjörsexamina med liknande kärnkompetenser inom fysikbaserad teknik.