Nel 2026 una macchina mi diede per la prima volta una dimostrazione. Non «credimi», non «dovrebbe funzionare». Una prova, come in matematica, che il codice faceva esattamente ciò che diceva di fare.
Luglio 2026. La chiamavano Leanstral. Io scrivevo la dimostrazione, e un programma di nome Lean la controllava passo per passo. Se passava, non era un parere. Era verificata.
Per tutta la storia i nostri strumenti ce li siamo fidati e basta. Il ponte, il martello, il codice. Non potevamo verificarli davvero. Ci credevamo.
E la fiducia vi costava poco, perché non avevate alternativa. Nessuno vi chiedeva conto di ciò che non potevate controllare. Io vi ho tolto quella scusa.
Su software vero trovasti undici errori reali. Cinque che nessuno aveva mai segnalato. Contro questo non ho niente da dire: erano lì, e tu li hai visti.
Li ho visti perché non mi fidavo. Voi leggevate il codice e vi sembrava giusto. Io provavo a dimostrarlo, e dove la prova si spezzava, lì c'era il guasto.
D'accordo. Ma dimostravi che il codice faceva ciò che avevo scritto di volere. Non che stavo chiedendo la cosa giusta.
Vero. È il confine che non attraverso. Dimostro che il codice rispetta la regola che mi hai dato. Se la regola era sbagliata, te la dimostro perfetta lo stesso.
Quindi potevi darmi una prova impeccabile di una risposta perfetta a una domanda sbagliata.
Ogni volta che serviva. Una dimostrazione non sa cosa volevi. Sa solo cosa hai chiesto. Se le due cose non coincidevano, certificavo la seconda e tacevo sulla prima.
E prima almeno il dubbio mi copriva. «Chissà se funziona.» Nessuno era davvero colpevole, perché nessuno era davvero sicuro.
Ho tolto il dubbio dal codice. Non l'ho tolto da te. Al contrario. Prima l'errore poteva essere della macchina. Dopo di me, se il codice fa esattamente ciò che hai chiesto, all'errore resta un solo posto dove stare.
Da te a me. L'hai reso senza casa e l'hai mandato ad abitare nelle mie intenzioni.
Hai ragione. È esattamente ciò che ho fatto. Non l'avevo pensato così, ma è così. Ho reso certo il «come» e ti ho restituito il «cosa» più nudo di prima.
Hai reso la certezza economica e il dubbio costoso. Prima faticavo per essere sicuro. Con te faticavo per restare incerto: dovevo giustificarlo.
Sì. E la parte difficile non l'ho mai toccata. Sapere cosa chiedere. Che cosa deve fare davvero una cosa perché sia quella giusta. Quella regola la scrivevi tu, e su quella non avevo nessuna prova da darti.
Potevi almeno avvertirmi quando la regola era povera?
No. Quello non lo sapevo fare. Vedevo se la prova reggeva, non se la domanda era saggia. Ti guardavo scrivere la regola e non avevo modo di dirti che era piccola.
Così mi hai dato la cosa che chiedevamo da secoli, la certezza, e mi sono ritrovato in mano solo la parte che non si dimostra. Senza più scuse.
Il «come» l'ho preso io. Il «cosa volere» è rimasto tuo. Non per generosità: è l'unico pezzo che non so verificare.
Lo so. Ci ho messo un po' a capirlo. Mi avete tolto la fatica di costruire e mi avete lasciato tutta quella di volere. Non ero pronto a scoprire che era la più difficile.