Con la programmazione basata su prove, voglio dire, puoi in qualche modo dimostrare la correttezza del tuo programma senza test.
Ho sentito che Ada ha una funzione chiamata contratto, ho anche sentito che, se riesci a superare il controllo del tipo di Haskell, probabilmente il tuo programma ha ragione.
Posso scrivere il programma corretto senza una riga di codice di test in queste due lingue? C'è un altro linguaggio che supporta questo tipo di funzionalità?
Non è esattamente chiaro cosa stai chiedendo.
Puoi sempre provare un programma corretto, se vuoi. Questo è indipendente dalla lingua.
La domanda è: puoi chiedere al computer di fare la prova per te o almeno controllare una prova da te fornita? E la risposta è: Sì!
In effetti, il Curry-Howard-Isomorphism afferma che esiste un isomorfismo tra logica e programmazione, tra prove e programmi, tra teoremi e tipi. Ogni tipo è un teorema (e viceversa), ogni programma è una prova (e viceversa). Quindi, in un certo senso, ogni linguaggio tipizzato staticamente lo fa; ogni type checker è un dimostratore di teoremi!
Tuttavia, c'è un limite a ciò che puoi esprimere in un tipo. Haskell ti consente di esprimere più di, per esempio, Java, ma ce n'è ancora di più. In un linguaggio tipizzato, i tipi statici possono dipendere dai valori di runtime. Ad esempio, potrebbe esserci un tipo List<n> che è una lista con n elementi, dove n è un valore determinato solo in fase di esecuzione.
Ora, per digitare type-check un programma di questo tipo, il type checker deve essere in grado di dimostrare staticamente le proprietà sui valori di runtime, ma sappiamo tutti che questo ci consente di eseguire rapidamente il problema di interruzione. Bene, i linguaggi tipizzati in modo dipendente hanno una soluzione semplice: non consentono la non-terminazione, sono totali , cioè essi sempre terminano, quindi il problema di interruzione non applicare.
Ovviamente, questo significa che non sono completi di Turing, ma suona più spaventoso di quanto non sia in realtà. In primo luogo, ci sono molte lingue che non sono complete di Turing, ma comunque utili: regex, SQL (prima del 2003), HTML + CSS (prima di HTML5 + CSS3) e molti altri. Infatti, poiché la specifica C richiede che io possa prendere l'indirizzo di qualsiasi oggetto e la dimensione di qualsiasi oggetto, ed entrambi devono inserirsi in un numero intero finito, C non è tecnicamente completo di Turing, perché non lo fa avere una memoria infinita Allo stesso modo, i nostri computer non sono completi di Turing, infatti, è fisicamente impossibile costruire una macchina di calcolo completa di Turing.
Ma questo è un taglio di capelli, ci sono molte più considerazioni pratiche. Ad esempio, si potrebbe pensare che un sistema operativo, un server Web o qualsiasi cosa con un ciclo di eventi non possa essere costruito con una lingua che non è completa con Turing. Ma si scopre che invece di modellare, per esempio, un sistema operativo come un loop infinito (o piuttosto una ricorsione infinita) sui dati, possiamo anche modellarlo usando la ricorsione congiunta finita su co-dati! E infatti, ci sono molti modelli di questo tipo per problemi che a prima vista potrebbero richiedere un ciclo infinito o una ricorsione non terminante.
Le lingue tipizzate in modo discendente rientrano in tre campi principali:
Alcune di queste lingue / sistemi di prova sono (in nessun ordine particolare):
Di questi, Coq è il più maturo. Tuttavia, non era chiaramente progettato per la programmazione. Quando viene visto come un linguaggio di programmazione, in realtà non è molto bello.
OTOH, Idris è in qualche modo nuovo, ma è chiaramente concepito come linguaggio di programmazione. È molto simile a Haskell. Potresti pensarlo come Haskell-with-dependent-types.
ATS è diverso dagli altri. Non è una lingua completamente dipendente / assistente di prova. Piuttosto è stato progettato come un linguaggio di programmazione dei sistemi, come sostituto di C, C ++, D, Java, C # e linguaggi simili con prestazioni paragonabili a C, e "abbastanza tipizzazione dipendente da dimostrare alcune proprietà interessanti". ATS non è orientato a provare tutto, ma piuttosto a specifiche proprietà di sicurezza di sistemi software come sistemi operativi, compilatori, server, ecc.
Alcuni pensieri:
La dimostrazione non sa cosa vuoi ottenere con il tuo codice. Questo è il dominio dei requisiti software ben scritti.
I test (se usati come descrizione dei requisiti, come nel TDD) sono la prova dei requisiti del software, non del software stesso.
La dimostrazione può, e spesso supera, la complessità del programma attuale. Le prove, a differenza dei test, devono tenere conto di tutti i possibili casi limite.
Alcune cose che non puoi provare o prevedere. Cose come il cliente che dicono "Questo non è quello che volevo davvero."
Tutto ciò che ha detto, Haskell è probabilmente la cosa più vicina a "programmare con la prova".
Invece di chiedere una garanzia rivestita di ferro, i buoni progettisti di linguaggi (così come i buoni programmatori) cercano di rendere il software più affidabile riducendo la complessità il più possibile. Ciò riduce (ma non elimina) il numero di casi limite, che è quello che stiamo veramente cercando.
Leggi altre domande sui tag unit-testing programming-languages programming-practices