Ich lerne gerade über Modellprüfung (Modallogik, LTL, CTL, SAL Model Checker, etc.) und in meiner Freizeit lerne ich über Idris, die eine stark typisierte funktionale Programmiersprache ist, die abhängige Typen unterstützt. Da ich sowohl Model Checking als auch Idris betrachte, beginne ich neugierig zu werden, wie sich Idris auf Formale Methoden und Model Checking bezieht.Relevanz der Modellprüfung in stark typisierten funktionalen Programmiersprachen?
Wenn man etwas über Modellüberprüfung erfährt, fühlt es sich an, als ob die meisten vorgestellten Beispiele entweder die Überprüfung von imperativ geschriebenen Systemen oder Hardwarekomponenten sind. Daher bin ich verwirrt über die Relevanz der Modellüberprüfung in stark typisierten funktionalen Programmiersprachen und insbesondere in einer abhängig typisierten Sprache wie Idris, wo es mir scheint, dass der Typüberprüfer bereits eine fantastische Arbeit bei der Überprüfung der Korrektheit leistet. Meine Intuition sagt mir jedoch, dass Model Checking vielleicht für partielle Funktionen relevant ist, die keine Beendigungsversprechen geben.
Ist die Modellprüfung relevant, wenn eine stark und abhängige Programmiersprache wie Idris verwendet wird?