Sto rileggendo questo link documento e prendo nota di questa riga,
'... Sfortunatamente, provare i programmi corretti è in gran parte poco pratico e non rilevante per il software Python. Persino i programmi banali richiedono prove lunghe diverse pagine; la dimostrazione di correttezza per un programma moderatamente complicato sarebbe enorme, e pochi o nessuno dei programmi che usi quotidianamente ( l'interprete Python , il tuo parser XML, il tuo browser web) potrebbero essere dimostrati corretti. Anche se annotassi o generassi una prova, ci sarebbe allora la questione di verificare la prova; forse c'è un errore e credete erroneamente di aver provato il programma corretto.
/ Enfasi mine sulla parte dell'interprete Python /
Che cosa significa che l'interprete Python non può essere dimostrato corretto? È perché sarebbe una prova lunga o che in linea di principio non può essere dimostrato corretto, ala Godel come teorema? Sta usando l'Interprete quindi una finzione utile che per tutto il tempo che la usiamo, potrebbe essere sbagliata per tutto il tempo, e cosa sarebbe sbagliato? Voglio dire, l'interprete mi ha dato risposte corrette sull'aritmetica integrale, finora ...
Chiarimento molto apprezzato.