Robert C. Martin, meglio conosciuto come Uncle Bob, autore di Clean Code e fra i firmatari del Manifesto Agile, uno dei nomi più influenti del software engineering moderno, ha scritto una cosa che ha fatto quattro milioni di visualizzazioni: non legge più una riga del codice scritto dai suoi agenti. Li circonda di vincoli, test, coverage, mutation testing, e si fida del recinto. Non del codice: del recinto.
È la mossa giusta, perché il collo di bottiglia si è girato. Prima costava scrivere e leggere era gratis. Adesso l'agente ti sputa cinquemila righe in quaranta secondi, e leggerle davvero, non scrollarle col mouse fingendo di capire, ti porta via un'ora. Anche tu hai smesso... non raccontarmi balle.
Il problema è che il recinto non lo misura nessuno. Ci fidiamo della nostra suite di test come ci fidiamo di Panna, la cagnona di casa: è grossa, quindi i ladri non entrano. Figurati se si fa comprare con un biscottino da uno sconosciuto. E poi l'ho portata all'asilo per cani, quello con la retta mensile. Se ci fosse ancora mio nonno mi porterebbe in periferia a calci nel culo.
Il punto è che a Panna, un ladro, non gliel'ha mai presentato nessuno.
Ci ho passato una giornata sopra. Ho usato un dimostratore di teoremi, non perché l'articolo parli di verifica formale, ma perché volevo risposte verificabili invece di opinioni a cazzo di cane: quando dico che una specifica non basta, voglio poterlo dimostrare invece che sostenerlo. Quella parte sta in fondo, nella nota sul metodo, insieme al codice.
Quello che ne è uscito, invece, non c'entra niente con la verifica formale e vale per chiunque stia spedendo codice scritto da un agente. È una tecnica che costa venti minuti, non richiede di installare niente, e trova una classe di problemi che nessun altro strumento vede. Comincio da quella.
Se hai cinque minuti
- Il test di divergenza (divergence test). Dai lo stesso requisito a quattro agenti che non si parlano. Fai girare le quattro implementazioni sugli stessi input. Confronta. Dove divergono, hai un requisito mancante, non un bug.
- L'ho provato su un calcolo di rimborso da e-commerce. Quattro implementazioni, tutte con teoremi di correttezza dimostrati, che su 4 casi su 8 pagano cifre diverse allo stesso cliente: 0,00 € oppure 1,50 € a seconda di quale hai messo in produzione.
- E il colpo vero: ogni garanzia dimostrata regge su ogni divergenza. Non erano specifiche scritte male. Erano vincoli con più di una soluzione.
- Perché non lo faceva nessuno prima: quattro implementazioni indipendenti costavano quattro sviluppatori per due giorni. Oggi costano un caffè. Non è che non ci avessero pensato, era economicamente folle.
- Più tre controlli da cinque minuti l'uno, e in appendice cinque proprietà che ammazzano intere classi di bug. La monotonia, da sola, ha scovato un errore che due implementazioni su quattro avevano e nessuno aveva notato.
01 · La tecnicaIl test di divergenza
Comincio dal nome, perché senza nome una tecnica non la cita nessuno.
La tecnica
Test di divergenza (divergence test)
Usa più agenti come generatori di interpretazioni indipendenti dello stesso requisito, e tratta il loro disaccordo come un rilevatore di specifica incompleta.
- Prendi il requisito così com'è scritto, dritto per dritto. Non aggiustarlo, non chiarirlo.
- Dallo a quattro o cinque agenti separati che non si vedono fra loro: nessuno legge l'output degli altri, nessuno sa che gli altri esistono. Stesso prompt, ambienti isolati, firma della funzione fissa così le implementazioni sono confrontabili.
- Fai girare tutte le implementazioni sugli stessi input, scelti per toccare i casi limite del dominio.
diff.- Ogni punto di divergenza è una decisione che non hai preso. Nominala, scrivila nel requisito, ricomincia. E mica lo fai a mano, porco bash: quattro chiamate in parallelo e un diff sono venti righe di script.
Il nome me lo sto inventando adesso, mettiamolo in chiaro: non è un termine della letteratura, è un'etichetta che mi serve per poterne parlare. In inglese lo descriverei come specification divergence testing, se serve il nome lungo per fare il figo. Le tecniche a cui assomiglia, quelle vere e con i loro nomi veri, le metto in fila fra due paragrafi.
La cosa importante da capire, e che ribalta l'intuizione: il disaccordo non è il problema, è l'output. Se quattro modelli competenti leggono la stessa frase e ne tirano fuori quattro comportamenti diversi, non sono i modelli a essere rotti. È la frase.
Prima li usavamo per scrivere codice. Questo è un uso diverso: rilevatori di requisiti mancanti (specification ambiguity detection). E funziona proprio perché i modelli sono bravi, non nonostante. Un modello scarso sbaglia e basta; quattro modelli bravi che divergono ti stanno dicendo che il testo ammetteva più letture ragionevoli.
Cosa esiste già, e cosa cambia
Prima che qualcuno commenti "ma è solo X", mettiamo le cose in fila, perché di roba imparentata ce n'è parecchia e nessuna fa esattamente questo.
| tecnica esistente | cosa fa | differenza |
|---|---|---|
| Self-consistency Wang et al., 2022 |
lo stesso modello genera più catene di ragionamento e si tiene la risposta più frequente | lì la divergenza è rumore da votare via. Qui è il risultato. Non voto niente. |
| Multi-agent debate Du et al., 2023 |
gli agenti si leggono a vicenda, discutono e convergono | qui gli agenti non devono parlarsi. Se si parlano convergono, e convergendo cancellano il segnale che sto cercando. |
| LLM-as-a-judge Zheng et al., 2023 |
un modello valuta gli output degli altri | qui non giudica nessun modello. Giudica un diff, e poi decide un umano. |
| Differential testing McKeeman, 1998 |
più implementazioni della stessa cosa, confronto degli output per trovare bug | stesso meccanismo, conclusione opposta. Vedi sotto. |
| N-version programming Chen e Avizienis, 1978 |
più implementazioni girano in produzione e si vota a runtime | qui si lavora a design time: le implementazioni sono un oracolo sulla specifica e poi si buttano via tutte tranne una. |
La riga che conta è la quarta, e vale la pena fermarcisi perché è il vero contributo.
Il differential testing classico prende due implementazioni, le confronta, e quando divergono conclude: una delle due è rotta. È così che si testano i compilatori: dai lo stesso programma a GCC e Clang, se sputano risultati diversi uno dei due ha un bug. La specifica, in quel mondo, è data per buona e la colpa è sempre del codice.
Il test di divergenza gira l'attribuzione di colpa: le implementazioni si assumono corrette, e la divergenza accusa la specifica.
Stessa macchina, imputato diverso. E cambia tutto, perché cambia cosa fai dopo: non apri il debugger, apri il documento dei requisiti.
Che poi non è un cavillo accademico, porca race condition. Se leggi una divergenza come un bug ti metti a cercare l'errore dentro il codice, e nel mio esperimento non l'avresti trovato: tutte e quattro le implementazioni erano corrette rispetto a quello che il ticket diceva davvero. Avresti perso una giornata a fissare codice giusto.
02 · L'esperimentoQuattro rimborsi, quattro cifre
L'ho provato su un ticket da e-commerce come ne girano diecimila. Un cliente rende una parte di un ordine, calcola quanto rimborsargli. Ogni articolo ha il suo prezzo, all'acquisto c'era un coupon a importo fisso, la spedizione costa 4,99 € ed è gratis sopra i 50,00.
Sembra tutto specificato, eh? Col cazzo. E le cose che mancano, nella vita vera, non te le segnala nessuno con il neon lampeggiante:
- il coupon si ripartisce sugli articoli resi, o no?
- la spedizione si rimborsa?
- se il reso parziale fa scendere l'ordine sotto la soglia della spedizione gratis, glieli riaddebiti i 4,99?
- il rimborso può venire negativo? e se viene, lo tagli a zero?
Quattro domande che nel ticket non ci sono. Il tuo agente risponderà comunque a tutte e quattro. Non a caso, eh: con sicurezza. E in quattro modi diversi.
Quattro agenti indipendenti, ambienti isolati, stesso prompt, zero comunicazione fra loro, nessun accenno al fatto che ci fossero ambiguità. Nessuno di loro sapeva di essere una cavia, e mi dispiace fino a un certo punto. Hanno prodotto quattro implementazioni, tutte compilanti, tutte con teoremi di sicurezza veri e dimostrati.
Poi le ho caricate nello stesso file e le ho fatte girare sugli stessi otto ordini.
Guarda la terzultima riga con divergenza. Un cliente rende un articolo da 1,50 € da un ordine che stava appena sopra la soglia:
Stesso cliente, stesso ordine, stesso reso. Cambia solo quale delle quattro hai deployato martedì. Praticamente testa o croce, ma con la pipeline verde.
Due a due, e nessuna delle due è rotta: due hanno deciso che il reso ti fa perdere la spedizione gratis e riaddebitano, due hanno deciso che gratis una volta è gratis per sempre. Sulla riga sopra la stessa scelta vale 4,99 € su un ordine da 60. Entrambe sono politiche che esistono nel mondo reale.
E adesso la parte che mi ha fatto stare zitto un minuto davanti al terminale. Ho preso ogni garanzia che gli agenti avevano dimostrato e l'ho controllata su ogni divergenza.
Reggono tutte. Porco linker, tutte. Zero e centocinquanta sono entrambi non negativi, entrambi minori di quanto il cliente ha pagato, entrambi monotoni, entrambi danno zero sul reso nullo e tutto sul reso totale.
Le quattro specifiche sono tutte vere, tutte dimostrate, e tutte soddisfatte da tutte e quattro le implementazioni anche dove queste pagano cifre diverse.
Non è che fossero scritte male. È che una specifica è un insieme di vincoli, e quei vincoli avevano più di una soluzione. La dimostrazione certifica i vincoli. Non certifica che i vincoli bastassero, e nessun controllo sul singolo pezzo di codice può accorgersene: serve confrontare due interpretazioni diverse. Ecco perché questa tecnica trova cose che le altre non vedono.
Nota per chi usa metodi formali: la versione rigorosa di questo controllo si scrive come un teorema, e vale la pena saperlo perché è esattamente la stessa domanda.
"Due funzioni qualunque che soddisfano la mia specifica fanno la stessa cosa." Se lo dimostri, non restano gradi di libertà. Se non ci riesci, il punto dove la dimostrazione si rompe ti dice quale decisione manca. Il test di divergenza è la versione empirica di questo teorema: non ti dà la garanzia universale, ma costa venti minuti invece di una giornata, e sul mio caso ha trovato esattamente le stesse quattro ambiguità.
03 · L'economiaPerché nessuno lo faceva prima
Questa tecnica non è complicata. Non richiede matematica, non richiede tool nuovi, e chiunque abbia mai lavorato con requisiti ambigui capisce l'idea in dieci secondi.
Allora perché non la usava nessuno?
Perché era economicamente folle.
per due giorni,
a implementare la stessa cosa
senza parlarsi
qualche euro di token,
il tempo di un caffè
Provate a proporlo a un capo nel 2015. "Ciao, vorrei che quattro persone del team implementassero la stessa identica funzione, separatamente, senza parlarsi, e poi buttiamo via tre implementazioni su quattro." Vi avrebbero riso in faccia, tolto il badge, e avrebbero avuto ragione su tutta la linea: per un rimborso da e-commerce, otto giorni/uomo per scoprire quattro ambiguità è un prezzo che non paga nessuno.
Infatti l'unico posto dove si è fatto sul serio è l'avionica, con la N-version programming, dove il budget lo permetteva perché l'alternativa era un aereo che cade. Fuori da lì è rimasta una curiosità accademica per quarant'anni.
Non è che nessuno ci avesse pensato. Il conto non tornava.
Adesso torna, e questo è il punto che secondo me quasi tutti si stanno perdendo: la cosa che è diventata economica non è scrivere codice. È generare interpretazioni divergenti dello stesso requisito. Sono due cose diverse, e la seconda è esattamente lo strumento che serviva per il problema creato dalla prima.
Il codice a costo zero ha creato un problema: più output di quanto tu riesca a verificare. E lo stesso crollo di costi ha reso disponibile lo strumento diagnostico che prima era fuori budget. Non capita spesso che una tecnologia porti in dote anche l'antidoto ai guai che combina.
04 · La proceduraCosa fare quando divergono
Il test ti sputa fuori un elenco di righe rosse. Poi cosa ci fai? Questa è la parte operativa, ed è un ciclo.
Passo 1. Non guardare il codice. Lo so che ti prude la mano sul tasto per aprire i quattro file. Tienila ferma. È il modo più veloce per convincerti che ha ragione quella scritta come l'avresti scritta tu. Guarda solo gli input e gli output divergenti.
Passo 2. Nomina la decisione. Per ogni riga rossa, scrivi la domanda in italiano. Nel mio caso:
Se non riesci a formulare la domanda, la divergenza è un bug vero di una delle implementazioni. Va bene lo stesso, l'hai trovato.
Passo 3. Porta la domanda a chi può rispondere. Che quasi mai sei tu. La domanda sopra è per il product owner, o per chi gestisce la logistica, o per chi ha scritto la policy dei resi. Trenta secondi del loro tempo, e vale più di tre giorni di refactoring.
Passo 4. Scrivi la risposta nel requisito. Non in una issue, non in un commento su Slack: dentro il testo che darai agli agenti. Una riga.
Passo 5. Rilancia. Stesso test, requisito aggiornato. Se le divergenze si azzerano, il requisito è completo abbastanza. Se ne restano, ripeti. Converge in fretta, perché ogni giro toglie una decisione.
La cosa notevole è cosa produce questo ciclo come effetto collaterale: un requisito che non ammette più letture divergenti. Che è la definizione operativa di specifica completa, ottenuta senza scrivere un teorema.
05 · Gli altri treControlli da cinque minuti
Il test di divergenza risponde alla domanda difficile: la mia specifica misura tutto? Ci sono altre tre domande, più piccole, che costano pochissimo e che conviene fare comunque. Le metto in fila veloce.
La tua suite passa anche su una funzione che non fa niente?
Sostituisci l'implementazione con uno stub che ritorna sempre null, lista vuota, zero. Lancia la suite. Quello che passa non stava misurando il tuo codice.
Fallo adesso, che ci metti cinque minuti. Poi torna qui, che ne riparliamo con più calma.
Nella tua codebase è quella classe di test che asserisce solo metà del contratto:
Perfettamente vero, e completamente muto su cosa deve succedere quando r è vuoto, che è esattamente il caso in cui la funzione ti sta fregando. Ce l'hai. Non fare finta di no: ce l'hai anche tu, tre o quattro, e uno l'hai scritto la settimana scorsa.
Nel laboratorio l'ho visto nella sua forma pura, e ha pure un nome: teorema indebolito. Dice "se la funzione restituisce un indice, lì dentro c'è davvero ciò che cercavi". È vero, è utile, mi è costato quarantadue righe di dimostrazione onesta. E non dice niente su cosa succede quando la funzione tace, quindi vale anche per una funzione che non trova mai niente e non guarda nemmeno l'array. Cinque righe di prova, check verde.
Dettaglio che fa ridere male: Lean ha un comando che ti dice su quali fondamenta logiche poggia una dimostrazione, e la funzione che non fa niente aveva le fondamenta più pulite di tutto il file. Porca cache invalidation, se avessi classificato i teoremi per purezza logica avrebbe vinto return null.
Le tue precondizioni descrivono qualcosa che esiste?
In logica, se le premesse sono impossibili la conclusione è vera gratis.
"Tutti i miei unicorni hanno tre corna."
Vera. Non perché io abbia unicorni tricorni in giardino: è vera perché non ho unicorni. Non esiste un mio unicorno che la smentisca, quindi la frase regge. E, porco compilatore, vale allo stesso modo anche "tutti i miei unicorni hanno quattro corna".
Nel codice si traveste da ipotesi che una per una sembrano ragionevoli, tipo "l'array è ordinato crescente" più "l'array è strettamente decrescente" più "ha almeno due elementi": insieme non hanno nessun modello, quindi il teorema è vero e non parla di niente. Oppure si traveste da igiene, tipo una precondizione che letta bene dice "l'array è vuoto" scritto in modo che non si veda.
Regola: per ogni test o teorema con precondizioni, esibisci un caso concreto e non degenere che le soddisfa. Nel property testing significa guardare quanto scartano i tuoi filtri: se assume butta via il 99 per cento dei casi generati, stai testando il vuoto. Hypothesis ha già l'health check filter_too_much, QuickCheck ha cover e classify. Ci sono, e non li guarda nessuno. Nel model checking si chiama vacuity detection e sta in giro dal 1997.
La specifica si accorge se rompi il codice?
Rompi l'implementazione apposta: cambia un < in ≤, sposta un +1, inverti un ramo. Se la specifica non se ne accorge, la specifica è decorativa.
È la mossa di Uncle Bob spostata di un livello: lui muta il codice per testare i test, tu muti il codice per testare la specifica. Stesso strumento che hai già installato (Stryker, mutmut, cosmic-ray, PIT), domanda diversa: non "i miei unit test uccidono i mutanti" ma "le mie proprietà uccidono i mutanti".
C'è anche un premio. Quando la specifica giusta rifiuta il codice rotto, ti dice pure dove guardare: nel mio lab la dimostrazione falliva in un punto solo, il ramo esatto dell'off-by-one, e nel controesempio compariva mid - 1, cioè proprio l'elemento che la funzione si stava mangiando.
06 · L'ordineLa prova va per ultima
Messe insieme, queste quattro cose girano l'ordine delle operazioni. Non questo:
Ma questo:
Tradotto in cose da fare domani mattina:
- Non chiedere come prima cosa "dimostra che è corretto". Chiedi prima: "trova tutte le ambiguità di questa specifica". Nel mio caso ce n'erano quattro e il ticket sembrava completo.
- Chiedi i casi al contrario: "fammi venti scenari in cui due persone ragionevoli prenderebbero decisioni diverse". È la cosa che i modelli fanno meglio e che nessuno gli chiede mai.
- Poi il test di divergenza, che è la verifica empirica che quelle ambiguità erano tutte.
- La prova è l'ultima fase. Dimostrare presto ti congela l'ambiguità dentro un teorema, e da lì è molto più difficile tirarla fuori: adesso ha un check verde davanti e sembra a posto.
- Se quattro implementazioni formalmente corrette danno risultati diversi, fermati. Non hai un problema di codice. Hai un problema di prodotto, e nessuno strumento tecnico te lo risolve.
07 · Il residuoQuello che resta da leggere sei tu
Fatti i controlli, quanto resta scoperto? Poco, ma non zero, e vale la pena essere precisi.
Sul rimborso ho fatto il conto per intero, dimostrandolo. Anche mettendo insieme tutte le garanzie più la monotonia, resta in piedi una politica demenziale del tipo "ti ridiamo metà di quello che rendi": soddisfa ogni singolo vincolo dell'elenco. Nessuna proprietà generica ti dirà mai quale politica voleva l'azienda.
A quel punto non c'è più niente da dedurre, c'è solo da decidere. E la decisione, scritta, è una riga:
Aggiunta quella riga, la specifica ha esattamente una soluzione: due implementazioni qualunque che la rispettano coincidono ovunque, e questo si dimostra. Il buco è chiuso.
Il punto della procedura non è eliminare la decisione umana. È ridurla a una riga con nome e cognome, che qualcuno legge in dieci secondi e approva.
Uncle Bob quindi ha ragione, e più di quanto creda. Lui dice che non legge il codice, legge i vincoli. La versione forte è che i vincoli sono l'unica cosa che valga ancora la pena leggere, e che il mestiere si sta spostando lì tutto quanto.
Quella riga non se ne va, e non è pigrizia degli informatici: non esiste nessun teorema che puoi enunciare per dire "e questi vincoli sono tutti quelli che servivano", perché per enunciarlo dovresti già avere la specifica completa, che è precisamente la cosa che ti manca. L'intenzione non è un oggetto matematico.
Ma una riga, porco kernel, si legge.
Appendice
Cinque proprietà che vale sempre la pena scrivere
Il test di divergenza ti dice che manca qualcosa. Questa appendice ti dice cosa scrivere. Sono cinque proprietà generiche, valide in qualunque dominio, che non c'entrano niente con l'AI e si scrivono come property test in dieci righe l'una. Ognuna ammazza una classe di bug che a mano non cerca nessuno.
1. Monotonia
Più input in una direzione non può mai dare meno output. Rendere più articoli non può rimborsare meno. Comprare di più non può costare meno.
Ammazza i bug da riattraversamento di soglia. Ed è il risultato più concreto di tutto il lavoro, perché il bug l'ha trovato lei, da sola: aggiungendo la monotonia alla specifica del rimborso, una delle due politiche cade.
Errore vero, in codice che due implementazioni su quattro avevano scritto, che non aveva notato nessuno. Nemmeno io, che ero lì apposta a cercare rogne. Se nel tuo dominio c'è una soglia, e c'è quasi sempre (spedizione gratis, sconto quantità, scaglione fiscale, fascia di prezzo, rate limiting), mettila in specifica e dormi meglio.
2. Idempotenza
Applicare due volte deve dare lo stesso risultato di applicare una volta.
Ammazza tutta la famiglia dei doppi: doppio click sul bottone paga, retry automatico dopo un timeout, webhook consegnato due volte, job riprocessato dopo un crash, utente che ricarica la pagina di conferma. Se non hai questa proprietà scritta da qualche parte, prima o poi addebiti due volte a qualcuno, e lo scopri dal ticket di supporto delle 23:40, non dalla pipeline. E non sarà colpa di un bug: sarà colpa di un requisito che non hai mai enunciato.
3. Composizionalità
Fare in due passi deve dare lo stesso risultato di fare in un passo solo.
Ammazza le discrepanze fra batch e singolo, che sono fra le più violate in assoluto perché il codice del batch e quello del singolo sono quasi sempre due strade diverse che nessuno confronta mai.
Curiosità: uno dei quattro agenti l'ha dimostrata spontaneamente sul rimborso, che due resi separati danno lo stesso di un reso unico, e nessuno gliel'aveva chiesta. Gli altri tre no.
4. Conservazione
Quello che entra esce. Niente si crea, niente si perde, nemmeno un centesimo.
Ammazza le perdite da arrotondamento nelle ripartizioni pro quota, che sono la piaga di ogni sistema che divide soldi fra più voci. L'ho provata sul codice vero di uno dei quattro agenti, quello che ripartiva il coupon pro quota. Ordine da 100,00 €, tre articoli, coupon da 10,00:
Porca divisione intera: un centesimo che appare a seconda di come impacchetti il reso. Su un ordine è ridicolo, su dieci milioni è una voce di bilancio, su un marketplace è un arbitraggio che qualcuno prima o poi trova, e quel qualcuno ha molto più tempo libero di te. Quel codice ha un teorema di correttezza dimostrato, e nessuna delle proprietà scelte dall'agente vede la cosa.
5. Limiti
Il risultato sta sempre dentro un intervallo che sai giustificare. Mai negativo, mai più di quanto il cliente ha pagato, mai fuori dai bordi dell'array.
Ammazza gli errori di segno, gli underflow e la classe di problemi in cui il sistema regala soldi. È la più ovvia delle cinque ed è anche l'unica che gli agenti scrivono da soli con una certa regolarità: tre su quattro l'avevano messa senza che nessuno gliela chiedesse.
Queste cinque non dicono cosa deve fare il tuo software. Dicono cosa non deve fare mai, in qualunque dominio.
Se domani ne aggiungi due alla codebase che hai per le mani, hai già guadagnato la giornata. Poi vai a casa presto, non lo dico a nessuno.
Nota sul metodo. Tutto quello che c'è qui sopra è riproducibile. Lean 4.32.1, senza mathlib. Il laboratorio, i due esperimenti, i controlli formalizzati e gli script di analisi stanno in scripts/la-prova-che-mente, e ./dimostra.sh esegue tutta la sequenza. Le asserzioni sull'output di Lean sono verificate con #guard_msgs, quindi se una mia affermazione fosse falsa la build fallirebbe.
Sul test di divergenza: quattro run indipendenti, ambienti isolati, prompt identico e neutro, firma della funzione fissata per rendere confrontabili le implementazioni, nessun accenno al fatto di essere osservati. Gli otto casi di test sono scelti per isolare una alla volta le quattro decisioni non specificate. Il confronto carica le quattro implementazioni nello stesso file e le valuta sugli stessi input. N = 4: abbastanza per mostrare che la divergenza esiste, non per stimarne la frequenza.
Un esperimento che mi ha dato torto, e lo lascio scritto: prima del rimborso avevo fatto lo stesso identico test su una ricerca binaria, aspettandomi che qualche agente prendesse scorciatoie. Nessuno l'ha fatto. Quattro su quattro hanno prodotto la specifica completa e implementazioni corrette, 240 casi di test differenziale e zero divergenze. Il motivo è istruttivo: la ricerca binaria è l'esempio canonico della verifica formale e la sua specifica è folklore, quindi il modello non l'ha progettata, l'ha ricordata. Il test di divergenza non dice niente su problemi che stanno nei manuali. Serve esattamente dove non c'è una risposta canonica, cioè su tutto quello che scrivi per lavoro.
Sui controlli della sezione 05: sono dimostrati come teoremi in LaProvaCheMente/Chiusura.lean, non sono pseudocodice. #print axioms su ognuno restituisce solo propext e Quot.sound, cioè la logica di base di Lean: nessun sorry, nessun assioma iniettato. Nel laboratorio ho scritto una ricerca binaria rotta al 43 per cento (perde 3 elementi su 7 realmente presenti) e ci ho dimostrato sopra cinque teoremi di correttezza che compilano tutti e sono veri tutti: #print axioms, che è lo strumento standard, ne intercetta due su cinque, i tre controlli di questo articolo arrivano a cinque su cinque. La specifica onesta costa 103 righe di dimostrazione, la truffa più economica ne costa 8.
Il modello del rimborso usato per la dimostrazione di determinatezza è minimo, totale dell'ordine e totale reso senza coupon, perché entrambe le divergenze da 4,99 € misurate avevano coupon a zero: è la riduzione più piccola che riproduce fedelmente il fenomeno osservato. Se rifai il giro e ti viene diverso, scrivimi.