Ultimamente ho letto molto e ho trovato articoli in cui le persone affermano che non ci sono errori nel programma Tex di donald knuth. È questo in ogni modo possibile e se sì, come è possibile?
(anche se è stato contrassegnato come duplicato, la mia risposta non è;)
È possibile ma nessuno può dimostrarlo, non per le dimensioni di TeX. link è un esempio di software verificato.
Ci sono due cose che chiunque può fare per dire che il loro software è privo di bug (non dicendo che Don lo abbia detto):
Il problema con (1) è anche se un software ha superato il test, non ci sono ancora prove che non ci siano errori. Dimostra solo che il programma non ha bug che verrebbero rilevati dal set di test. Per il programma di grandi dimensioni, il costo del test sarebbe troppo alto. TeX ha goduto fondamentalmente di test gratuiti dalla sua base di utenti. Se Don potesse dimostrare che TeX è privo di bug, potrebbe aver messo una taglia in milioni di dollari.
Il link che ho messo lì è un esempio di (2) come può essere provato un programma di dimensioni ragionevoli. Per ragionevole intendo, può fare qualcosa di utile, non un programma di linea che ha una prova banale. Quello che hanno fatto è che hanno progettato, perfezionato il design e tradotto il design in C e hanno fatto controllare i passaggi del teorema (Isabelle / HOL). La dimensione della parte comprovata è di 7500 righe di codice C.
Probabilmente sarebbe troppo difficile far sì che tutti i programmi siano costruiti come un sistema affidabile, ma è ipotizzabile che alcune parti di un programma siano verificate e che i test coprano le parti rimanenti del programma.