Czy teoria typów Martina-Löfa przyczyni się do większej zdolności do pisania poprawnego kodu, który da się udowodnić

Ten post odnosi się do izomorfizmu Curry'ego-Howarda i teorii typów Martina-Löfa .

W postie stwierdza się o przyszłym „zjednoczeniu” języka opisu matematyki z językiem programowania komputerowego opartym na operacjach.

Moje pytania to:

1. Czy te pomysły doprowadzą do lepszej zdolności (poprzez języki) do pisania możliwego do udowodnienia poprawnego kodu?

2. Czy pełne implikacje MLTT zostały odkryte na poziomie teoretycznym?

3. Czy ten post opisuje coś, czego nie można było zrobić w COQ lub Agdzie?

Nie sądzę, aby twoje pytanie było szczególnie dobrze postawione. Najczęściej prosi o opinie. Oto moje:

1. Tak.
2. Nie wiem, co masz na myśli, ale odpowiedź brzmi prawdopodobnie „jest jeszcze więcej teorii MLTT do zrobienia, choć wiemy dużo”.
3. Nie można wykonać wszystkich teorii typów homotopii w Coq i Agda. To jest aktywny obszar badań.