Czy system typów może służyć jako asystent dowodu dla funkcji zagranicznych?

Jeśli się uwzględni:

1. Język z bardzo ekspresyjnymi systemami typów (np. Idris ) może również mieć mechanizmy specjalne, takie jak interfejsy funkcji obcych / niebezpieczne SafePerformIO.
2. Istnieją asystenci sprawdzania, których można użyć do udowodnienia niektórych właściwości programu napisanego w języku, który nie ma systemu typów zdolnego do wyrażania tych właściwości.
3. Korespondencja Curry-Howard pokazuje, że udana implementacja funkcji z danym typem z potwierdzeniem typu jest dowodem na to, co wyraża ten typ.

Czy można wyrazić nietrywialne dowody posiadania jakiejś własności kodu języka obcego w systemie pisma w języku ojczystym?

Na przykład, udawaj, że mam funkcję C o nazwie stable_qsort, która sortuje liczby w strasznie sprytny i wydajny sposób, zachowując jednocześnie kolejność już równych elementów, oraz program Idris, który wywołuje stable_qsort za pośrednictwem swojego FFI, ale nie ufam tak stosunkowo niejasnemu Funkcja C. Czy mogę udowodnić, że funkcja nie zmienia kolejności równych elementów dla wszystkich danych wejściowych w moim kodzie Idris zamiast używać osobnego asystenta proof?

Krótko mówiąc: nie, nie możesz. Funkcja obca jest jak czarna skrzynka, a typ, który ją przypisujesz, jest złożoną obietnicą: w korespondencji Curry-Howarda, która odpowiadałaby dodaniu aksjomatu do twojej teorii.

Biorąc to pod uwagę, istnieją sposoby. Na przykład w Coq istnieją różne formalizacje standardu C (np. Praca Robberta Krebbersa ). Ponieważ masz wyraźną reprezentację programów C i ich semantyki, możesz napisać kod bezpośrednio w asystencie sprawdzania, a następnie można udowodnić niektóre z jego właściwości.