💻 computer science

AI for software engineering: from probable to provable

Il documento propone di superare le sfide del "vibe coding", come la difficoltà di specificare gli obiettivi e le allucinazioni dell'IA, integrando la creatività dell'intelligenza artificiale con il rigore dei metodi di specifica formale e la potenza della verifica formale dei programmi.

Autori originali: Bertrand Meyer

Pubblicato 2026-04-24

📖 4 min di lettura☕ Lettura da pausa caffè

CC BY 4.0

Autori originali: Bertrand Meyer

Articolo originale sotto licenza CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Questa è una spiegazione generata dall'IA dell'articolo qui sotto. Non è stata scritta né approvata dagli autori. Per precisione tecnica, consulta l'articolo originale. Leggi il disclaimer completo

🤖 L'Intelligenza Artificiale e il Codice: Dal "Probabilmente" al "Provabilmente"

Immagina che l'Intelligenza Artificiale (AI) sia un geniale ma distratto studente universitario. È brillante, legge tutto, è veloce, gentile e ti dà sempre risposte convincenti. Ma c'è un problema: a volte inventa le cose. In gergo tecnico si chiama "allucinazione", ma pensala come se lo studente stesse bluffando con sicurezza: ti dice la verità, ma a volte mescola i fatti con la fantasia.

Bertrand Meyer, un esperto di informatica, ci dice che l'AI sta cercando di rivoluzionare la programmazione con il "vibe coding" (codificare basandosi solo sull'idea vaga di cosa si vuole). Ma Meyer ha una domanda fondamentale: è sicuro affidarsi a uno studente distratto per costruire cose importanti?

Ecco i punti chiave, spiegati con delle metafore:

1. Il problema della "Richiesta" (Non è solo "Scrivi questo")

Molti pensano: "Basta dire all'AI cosa voglio e lei scriverà il codice!".
Meyer dice: "Ah, se solo fosse così semplice!".
Chiedere all'AI cosa vuoi è come chiedere a un architetto di costruire una casa senza disegni precisi. Devi spiegare esattamente cosa deve fare la casa. Se dici "voglio una casa bella", l'AI potrebbe costruirti una capanna di fango che sembra bella ma crolla.
In informatica, questo si chiama Ingegneria dei Requisiti. È la parte più difficile: definire con precisione assoluta cosa il software deve fare. Se la richiesta è vaga, il risultato sarà un disastro, anche se fatto da un'AI.

2. Il paradosso della "Cosa che sembra giusta"

L'AI è bravissima in cose come tradurre lingue o riconoscere foto. Se traduce una frase in modo quasi perfetto, va bene. Se riconosce un gatto in una foto ma lo confonde con un cane una volta su mille, va bene.
Ma con il software? Non va bene.

Analogia: Se un medico AI sbaglia una diagnosi su 100 pazienti, è ancora utile. Se un software di controllo del traffico aereo sbaglia un calcolo su 100 voli, tutti gli aerei si schiantano.
Il software è "tutto o niente": o funziona perfettamente, o è inutile (e pericoloso). L'AI, basandosi sulle probabilità ("la risposta più probabile"), non può garantire la perfezione matematica.

3. L'Effetto Valanga (Il problema dei moduli)

Immagina di costruire un castello di carte.

Se hai 10 carte e ognuna ha il 99% di probabilità di stare in piedi, il castello sta in piedi.
Se hai 5.000 carte (come in un grande software), anche con il 99% di probabilità per ogni carta, il castello crollerà quasi sicuramente.
L'AI produce codice che è "probabilmente corretto". Ma quando unisci migliaia di pezzi di codice "probabilmente corretti", il risultato finale è quasi sicuramente sbagliato.

4. La Soluzione: Il Matrimonio Perfetto

Meyer non vuole buttare via l'AI. Vuole sposarla con la Matematica.
Immagina due personaggi:

L'Artista (AI): Creativo, veloce, pieno di idee, ma un po' disordinato.
L'Architetto (Verifica Formale): Rigido, noioso, ossessionato dalle regole e dalla sicurezza.

La proposta di Meyer:
Facciamo lavorare insieme l'Artista e l'Architetto.

L'AI (l'Artista) suggerisce il codice e anche le regole (i "contratti" matematici) su come dovrebbe comportarsi.
L'Architetto (gli strumenti di verifica) controlla matematicamente se il codice dell'AI rispetta davvero le regole.
Se c'è un errore, l'AI lo corregge e riprova.

Questo processo si chiama "Vibe-Contracting" (un gioco di parole tra "vibe coding" e "contratti"). È come se l'AI scrivesse il romanzo, ma un editore matematico controllasse ogni singola frase per assicurarsi che non ci siano errori logici prima di stampare il libro.

5. Perché è importante?

Senza questo controllo matematico, l'AI sarà solo un assistente veloce per fare cose piccole e non critiche (come un'app per organizzare una festa). Ma per le cose importanti (banche, ospedali, aeroplani), abbiamo bisogno di certezza, non di "probabilità".

In sintesi:
L'AI è un motore potente, ma senza un volante matematico (la verifica formale), rischia di guidare dritto nel muro. La soluzione non è fermare l'AI, ma darle un "sistema di sicurezza" basato sulla logica matematica, così da passare dal dire "Sembra che funzioni" al dire "È matematicamente provato che funziona".

È un matrimonio tra la creatività dell'AI e la serietà della matematica: noioso forse, ma è l'unico modo per non avere incidenti.

Titolo: AI per l'ingegneria del software: dal probabile al dimostrabile

1. Il Problema: I Limiti della "Vibe Coding" e dell'IA Moderna

Il saggio affronta le sfide critiche nell'integrazione delle attuali tecniche di Intelligenza Artificiale (IA) nell'ingegneria del software, in particolare il fenomeno della "vibe coding" (codifica basata su prompt intuitivi). Meyer identifica due ostacoli fondamentali:

L'Ingegneria dei Requisiti come "Prompt Engineering": La premessa che l'IA possa generare codice semplicemente da una descrizione ("basta dire cosa serve") ignora la complessità dell'Ingegneria dei Requisiti (RE). Definire requisiti precisi è una delle discipline più difficili dell'ingegneria del software, spesso tanto complessa quanto la programmazione stessa. Requisiti vaghi o imprecisi porterebbero l'IA a generare codice che fa esattamente ciò che è stato chiesto, ma non ciò che è necessario.
Il Fenomeno dell'Allucinazione (Hallucination): A differenza di altri campi (come la traduzione o l'analisi delle immagini) dove un errore statistico è accettabile, il software richiede una correttezza quasi assoluta. L'IA moderna si basa su tecniche statistiche per produrre la risposta più probabile, non quella logicamente corretta. Questo porta a:
- Errori catastrofici: Codice che cancella file o introduce malware.
- Il "Caso Diabolico" (Hallucination Loop): Programmi difettosi che sembrano corretti. L'IA, basandosi sulla probabilità, può suggerire percorsi errati che appaiono plausibili, intrappolando lo sviluppatore in un ciclo iterativo di correzioni che peggiorano la situazione senza mai raggiungere la soluzione.

2. Metodologia: La Necessità di una Verifica Formale

Meyer sostiene che l'IA da sola non può garantire la correttezza del software a causa della sua natura probabilistica. La metodologia proposta per superare questi limiti è l'integrazione dell'IA con i metodi formali di specifica e verifica.

Specifiche Formali: È necessario passare da requisiti vaghi a specifiche matematiche precise (usando linguaggi come B, Alloy, o contratti in linguaggi come Eiffel o Dafny).
Verifica Statica: Utilizzo di strumenti di verifica formale (es. AutoProof, Dafny) che eseguono prove matematiche sul codice per dimostrare che soddisfa le specifiche, senza bisogno di eseguirlo (a differenza dei test dinamici).
Processo Iterativo Ibrido: Il futuro processo di sviluppo non sarà lineare, ma iterativo:
1. Generazione di bozze di specifiche e implementazione tramite IA.
2. Verifica formale delle incoerenze.
3. Correzione congiunta di specifiche e codice basata sugli errori di verifica (debugging tramite prove, non tramite test).
4. Ripetizione fino alla dimostrazione della correttezza.

3. Contributi Chiave

Distinzione tra Software "C" e "A/B": L'autore classifica i sistemi software in tre categorie:
- C (Casual): App demo, script semplici. Qui la "vibe coding" può funzionare perché la tolleranza agli errori è alta.
- A (Acuto) e B (Business): Sistemi critici e aziendali. Qui la correttezza è imperativa. L'IA non può sostituire l'ingegneria del software in questi ambiti senza un meccanismo di garanzia formale.
Il Paradosso della Correttezza Composta: Citando Dijkstra, Meyer evidenzia che in un sistema modulare, la probabilità che l'intero sistema sia corretto è il prodotto delle probabilità dei singoli moduli ( $p^N$ ). Anche con un'IA molto affidabile (es. 99.9% di correttezza per modulo), in un sistema di migliaia di moduli la probabilità di correttezza globale crolla a livelli inaccettabili. Solo la verifica formale può garantire la correttezza globale.
Sintesi Neuro-Simbolica: Propone un approccio che combina la creatività statistica dell'IA moderna con il rigore logico della verifica formale, definendo questo ibrido come l'unica via percorribile per scalare l'IA nell'ingegneria del software professionale.

4. Risultati e Osservazioni

Limiti dell'Approccio Attuale: Gli esperimenti mostrano che l'uso non supervisionato dell'IA porta spesso a cicli di allucinazione dove lo sviluppatore perde tempo a correggere errori che sembrano corretti. Inoltre, gli studenti che usano l'IA per generare codice spesso non sono in grado di spiegarlo o modificarlo, indicando una mancanza di comprensione profonda.
Potenziale dell'IA nella Verifica: Sebbene l'IA sia parte del problema (generando errori), può essere parte della soluzione. L'IA può aiutare a generare annotazioni complesse necessarie per la verifica formale (come invarianti di ciclo o di classe), che sono spesso il collo di bottiglia nell'adozione dei metodi formali.
Stato dell'Arte: La combinazione di IA e verifica formale è ancora in fase embrionale, con strumenti come AutoProof (per Eiffel) e Dafny che offrono prove di concetto, ma richiede un processo iterativo che unisce intuizione umana e rigore matematico.

5. Significato e Implicazioni Future

Il saggio conclude che il matrimonio tra IA e Ingegneria del Software è possibile, ma solo se si abbandona l'illusione che l'IA possa sostituire completamente la disciplina ingegneristica.

Dal Probabile al Dimostrabile: Il passaggio cruciale è spostare il paradigma da un software "probabilmente corretto" (basato su statistiche) a un software "dimostrabilmente corretto" (basato su prove matematiche).
Vibe-Contracting: Meyer conia il termine "vibe-contracting" (contrattazione tramite vibe) come complemento al "vibe-coding". Significa utilizzare l'IA non solo per scrivere codice, ma per co-sviluppare specifiche formali e implementazioni, verificando la coerenza ad ogni passo.
Impatto Economico e Professionale: Per i sistemi critici (A) e aziendali (B), l'IA non eliminerà i programmatori, ma cambierà il loro ruolo: da scrittori di codice a supervisori che guidano l'IA attraverso specifiche rigorose e verifiche formali, garantendo che la creatività dell'IA sia contenuta entro limiti di sicurezza e correttezza matematica.

In sintesi, Meyer sostiene che senza l'integrazione della verifica formale, l'IA rimarrà uno strumento utile solo per prototipi casuali, ma pericoloso e inaffidabile per l'ingegneria del software professionale. La soluzione risiede in un processo iterativo supportato da strumenti che trasformano la probabilità statistica in certezza logica.