|
|
Beschreibung |
KursbeschreibungIn den letzten 20 Jahren hat sich ein schleichender Paradigmenwechsel vollzogen: Stand früher die Korrektheit von Algorithmen und ihren Inkarnationen in Form von Programmen im Vordergrund, so ist heute Kundenzufriedenheit das Maß der Dinge. Dies liegt zum einen an der Natur der Probleme, deren programmierte Lösungen in den Mittelpunkt des Interesses gerückt sind, für die Korrektheit aber gar nicht definiert ist (wie z. B. Such- und Matching-Probleme, in jüngster Zeit auch generative KI in Verbindung mit Fragestellungen, deren Antworten naturgemäß subjektiv sind), zum anderen aber auch an den Geschäftsmodellen der Hersteller, die darauf bauen, dass es keine zugesicherten Eigenschaften gibt (hier ist Korrektheit ?nice to have?, aber keine Priorität). Denkt man an unsere ständig steigende Abhängigkeit von Software, ist dies ein unglückseliger Trend.
Mit diesem Seminar soll der Blick in die entgegengesetzte Richtung gewendet werden: Programme, die selbst einen Beweis darstellen. Beispiele für solche Programme sind typischerweise jene, die in deklarativen Sprachen geschrieben wurden, in denen mit einem Programm also nur das Problem beschrieben wird und die Lösung in der Ausführung der Beschreibung besteht. Prolog-Programme sind an sich ein gutes Beispiel hierfür; jedoch sind auch Prolog-Programme in der Regel nicht algorithmenfrei und es gibt keinerlei Garantien, dass ein Prolog-Programm fehlerfrei ist. Insbesondere der Umstand, dass Prolog keine Typen kennt, mag als Grund hierfür angeführt werden: Das Type Checking von Programmen ist nämlich die am weitesten verbreitete (und bis heute wohl erfolgreichste, wenn nicht einzige praktikable) Form der formalen Verifikation von Programmen.
Inhaltliche Voraussetzungen:
Gute Englischkenntnisse für die Literaturrecherche, gute Deutschkenntnisse für die Ausarbeitung, Interesse an theoretischen Inhalten. Praktische Programmiererfahrung in Funktionaler Programmierung sowie Kenntnis der Kurse 01816 (Logisches und funktionales Programmieren) und 01852 (Fortgeschrittene Konzepte funktionaler Programmierung) sind bei der Bearbeitung hilfreich.
Geforderte Leistungen: Eigene Literaturrecherche, Ausarbeitung in deutscher Sprache im Umfang von 20 Din-A4-Seiten Text plus Deckblatt, Inhaltsverzeichnis, Literaturverzeichnis, 20-25-minütiger Powerpoint-Vortrag, Beteiligung an der Diskussion zu den Vorträgen, Beteiligung an Austauschen zwischendurch.
|
|
|