I due sono cose diverse, e in effetti sono molto più diversi nella pratica di quanto non sarebbero in teoria.
Una prova formale di correttezza dimostra qualcosa sul comportamento di un algoritmo . Ad esempio, potrebbe investigare gli invarianti che si applicano ai dati mentre viene trasformato da un algoritmo di ordinamento e dimostrare che se l'algoritmo termina, ogni elemento è più grande del precedente. Questo tipo di prova può essere rigoroso, cioè se è fatto correttamente, l'algoritmo non può essere sbagliato a questo riguardo.
In pratica, gli algoritmi devono essere incorporati nel codice del computer e di solito non è fattibile provare che un dato bit di codice rappresenta esattamente l'algoritmo che si desidera. (Ciò richiederebbe una dimostrazione formale del comportamento del compilatore, della libreria standard, della macchina virtuale, ecc.) Diventa un po 'più facile, più il linguaggio di programmazione è simile alla notazione matematica che hai usato nella dimostrazione formale, ma non tanto. (Si diceva che il codice in esecuzione nei sistemi centrali dello Space Shuttle fosse quasi una perfetta notazione matematica, ma non molto piacevole da programmare.)
È molto più economico eseguire effettivamente il codice su input scelti con giudizio e verificare che produca i risultati attesi. Questo ha lo svantaggio che non si può mai essere certi che non ci sia un errore in esso - potrebbe comportarsi per quelle coppie di input / output non testate (e di solito ci sono più coppie di quelle che si possono testare, altrimenti non si Per prima cosa è necessario un programma per computer, o, peggio, il codice potrebbe essere sottilmente non deterministico o dipendente dal contesto in modo che i test non vengano esposti.
Ma in pratica, gli errori più che influiscono su un calcolo possono essere esposti con controlli intelligenti e se si tiene un registro degli errori noti e dei casi di test verificando che non possono ripetersi , la qualità del codice può essere generalmente adeguata a un valore aziendale. Certamente è un'idea migliore eseguire test unitari, test di integrazione e test di accettazione degli utenti e ottenere qualcosa fuori dalla porta che la gente pagherà piuttosto che condurre una lunga e costosa prova formale che trascura una sottile deviazione tra le specifiche scritte e attese del cliente. Quindi nel mondo reale, i due sono attività quasi completamente distinte.