Trafność sprawdzania modelu w mocno typowanych językach programowania funkcjonalnego?

Question

Obecnie uczę się sprawdzać model (logika modalna, LTL, CTL, sprawdzanie modelu SAL, itp.) Iw wolnym czasie uczę się o Idrisie, który jest silnie typowanym językiem programowania funkcjonalnego, który obsługuje typy zależne. Ponieważ patrzę zarówno na sprawdzanie modeli, jak i na Idris, zaczynam się zastanawiać, w jaki sposób Idris odnosi się do metod formalnych i sprawdzania modeli.

Podczas nauki o sprawdzaniu modelu, wydaje się, że większość przykładów dotyczy sprawdzania systemów napisanych w sposób naglący lub komponentów sprzętowych. Tak więc jestem zaintrygowany, jeśli chodzi o znaczenie sprawdzania modeli w mocno typowanych językach programowania funkcjonalnego, a zwłaszcza w języku, który jest zależny od pisowni, na przykład w Idrisie, gdzie wydaje mi się, że sprawdzarka typu wykonuje już fantastyczną pracę przy weryfikacji poprawności. Moja intuicja podpowiada mi jednak, że sprawdzenie modelu może mieć znaczenie dla częściowych funkcji, które nie dają żadnych obietnic rozwiązania.

Czy sprawdzenie modelu jest istotne w przypadku używania silnie zależnego języka programowania, takiego jak Idris?

Answer 1

Masz rację, że sprawdzenie modelu jest najczęściej używane do weryfikacji sprzętu i programów imperatywnych (często współbieżnych), ponieważ jego pochodzenie jest również w tym obszarze. W przypadku programów funkcjonalnych, szeroko stosowane techniki systemów typów są szeroko stosowane do weryfikacji. Jednak często wymagają one wielu adnotacji lub mogą generować "fałszywe alarmy", co skutkuje odrzuceniem "poprawnego" programu. Sprawdzanie modelu nie wymaga tych adnotacji, a także umożliwia udzielenie odpowiedzi na bardziej szczegółowe pytania. Nie jestem ekspertem w tej dziedzinie, ale wydaje się, że techniki z systemów typów i sprawdzania modeli są często łączone dla programów funkcjonalnych. Jeśli jesteś zainteresowany aktualnych badań i zbliża się do modelu sprawdzania programów funkcjonalnych, jest doskonały kurs z dużą ilością materiału ONLINE:

http://www.cs.ox.ac.uk/people/luke.ong/personal/EWSCS13

Kurs został przygotowany przez Łukasza Ong, jeden z wiodących naukowcy w tej dziedzinie.