Dijkstra w swoim eseju O okrucieństwie prawdziwego nauczania informatyki przedstawia następującą propozycję wprowadzenia kursu programowania:
Z jednej strony uczymy czegoś, co wygląda na rachunek predykatu, ale robimy to zupełnie inaczej niż filozofowie. Aby wyszkolić początkującego programistę w zakresie manipulowania nieinterpretowanymi formułami, uczymy go bardziej jako algebry boolowskiej, zapoznając studenta ze wszystkimi właściwościami algebraicznymi połączeń logicznych. Aby dodatkowo odciąć linki do intuicji, zmieniamy nazwy wartości {true, false} domeny boolean na {black, white}.
Z drugiej strony uczymy prostego, czystego, imperatywnego języka programowania, z pominięciem i wielokrotnym przypisaniem jako podstawowymi instrukcjami, ze strukturą blokową dla zmiennych lokalnych, średnikiem jako operatorem składu instrukcji, ładną alternatywną konstrukcją, ładnym powtórzenie i, jeśli to pożądane, wywołanie procedury. Do tego dodajemy minimum typów danych, np. Logiczne, liczby całkowite, znaki i łańcuchy. Istotne jest to, że niezależnie od tego, co wprowadzimy, odpowiednią semantykę określają reguły dowodu, które się z nią wiążą.
Od samego początku i przez cały czas podkreślamy, że zadaniem programisty nie jest tylko napisanie programu, ale że jego głównym zadaniem jest przedstawienie formalnego dowodu, że program, który proponuje, spełnia równie formalną specyfikację funkcjonalną. Projektując dowody i programy ręka w rękę, uczeń ma wiele okazji do doskonalenia swojej sprawności manipulacyjnej za pomocą rachunku predykatu. Wreszcie, aby przekazać wiadomość, że ten wstępny kurs programowania jest przede wszystkim kursem matematyki formalnej, dopilnujemy, aby dany język programowania nie został zaimplementowany w kampusie, aby uczniowie byli chronieni przed pokusą przetestowania swoich programów .
Podkreśla, że jest to poważna propozycja i przedstawia różne możliwe zastrzeżenia, w tym że jego pomysł jest „całkowicie nierealny” i „zdecydowanie zbyt trudny”.
Ale ten latawiec też nie poleci, ponieważ postulat okazał się błędny: od wczesnych lat 80-tych setki studentów pierwszego roku z powodzeniem organizowało taki wstępny kurs programowania. [Ponieważ, z mojego doświadczenia, powiedzenie tego raz nie wystarczy, poprzednie zdanie należy powtórzyć przynajmniej dwa razy.]
Do którego kursu odnosi się Dijkstra i czy jest dostępna inna literatura, która go omawia?
Esej ukazał się w 1988 roku, kiedy Dijkstra studiował na University of Texas w Austin, co jest prawdopodobnie wskazówką - są gospodarzem archiwum Dijkstra, ale jest ono ogromne i szczególnie interesują mnie informacje od innych o tym kursie.
Nie chcę dyskutować, czy pomysł Dijkstry jest tutaj dobry czy realistyczny. Zastanawiałem się nad opublikowaniem tego na cstheory.se lub cs.se, ale zdecydowałem się na to tutaj, ponieważ a) społeczność nauczycieli może mieć większą szansę na kogoś, kto może łatwo odpowiedzieć, i b) sam Dijkstra podkreśla, że jego kurs jest „przede wszystkim matematyka formalna ”. Jeśli się nie zgadzasz, możesz zgłosić flagę do migracji.