Bewertung des Praktikumsergebnisses

Typsysteme helfen Programmierern, Eigenschaften von Programmen über alle Ausführungen des Programms hinweg sicherzustellen. Je ausdrucksstärker das Typsystem ist, desto mehr Eigenschaften lassen sich auf diese Weise abdecken. Eine besonders ausdrucksstarke Klasse von Typsystemen sind solche mit abhängigen Typen. Bei diesen kann der Typ von Programmen von konkreten Laufzeitwerten abhängen. Das Programmieren in solchen Programmiersprachen erfordert theoretisches Wissen und vor allem praktische Erfahrung. Beides wird in diesem Praktikum vermittelt.

Die Studierenden wissen, was eine Programmiersprache mit abhängigen Typen ausmacht, welche zusätzliche Ausdrucksstärke auf der Typebene verfügbar ist und können diese praktisch in konkreten Programmen nutzen. Sie erkennen, welche Eigenschaften des Programms durch abhängige Typen sichergestellt werden können und welche Fehlerquellen vermieden werden können. Sie verstehen auch, welcher zusätzliche Aufwand dazu betrieben werden muss und können so eine informierte Entscheidung über die Nutzung einer Programmiersprache mit abhängigen Typen treffen.

-