traduzione italiana di "“Merging formal methods and agile development to build Cardano”
Pubblicato nel blog di IOHK il 9 Aprile, scritto da Philipp Kant , IOHK’s formal methods director.
Forma e funzione
IOHK sta costruendo Cardano come sistema operativo finanziario e sociale globale. Questo enorme compito richiede sia una rapida iterazione che una precisione assoluta. Per questo IOHK ha scelto di combinare la velocità di uno sviluppo agile con un codice di sicurezza e metodi formali di alto livello. La fusione di flessibilità e formalità ha portato i nostri ingegneri ad essere pionieri di questa moderna filosofia di sviluppo.
IOHK crede fermamente nella ricerca, nei metodi formali, nella programmazione funzionale e nella costruzione in modo rigoroso. In qualità di concorrenti nel settore dello sviluppo blockchain, dobbiamo anche dimostrare costantemente di progredire e creare valore per la nostra comunità globale di stakeholder. Ciò significa che non possiamo scendere a compromessi sulla robustezza, sulla velocità di sviluppo e sulla flessibilità. In un mercato in continua evoluzione questa è una sfida, quindi i nostri sviluppatori devono trovare un equilibrio.
Agilità contro formalità
Lo standard di partenza per lo sviluppo della nostra tecnologia è stato quello di costruire rapidamente un prodotto minimo vitale e poi iterare continuamente fino a quando non è pronto per il mercato di massa. Questo è noto come un processo agile. È un ottimo modo per dimostrare che un progetto sta avanzando mentre alla fine si costruisce un prodotto completamente funzionale. Tuttavia, una metodologia agile presuppone che ci saranno bug e punti deboli in ogni fase di sviluppo che possono essere risolti in seguito. Questo va bene se non c’è nessun valore a rischio - ma, con le valute virtuali, c’è un’enorme quantità di denaro e di fiducia degli stakeholder in gioco.
Costruire un asset digitale su una blockchain offre diverse sfide da superare in termini di organizzazione di un processo di sviluppo. Come valuta crittografica proof-of-stake, Cardano è un sistema distribuito in un ambiente conflittuale in cui la coerenza delle prestazioni è fondamentale. Il protocollo deve mantenere la sicurezza di fronte ad attori malintenzionati che tentano di sabotare l’intera rete. Ciò significa che nessuno può permettersi di costruire rapidamente e affrontare i problemi in seguito.
La fiducia è essenziale affinché una moneta sia accettata e le prove di correttezza sono un modo importante per aumentare la veridicità di un sistema. Questo è il motivo per cui il codice non solo dovrebbe essere corretto, ma ci dovrebbero essere prove della sua correttezza, come prove significative e prove matematiche. In un settore giovane come quello delle crittografie, gli ingegneri IOHK devono anticipare l’aggiunta di nuove caratteristiche mantenendo le garanzie di correttezza stabilite nella versione iniziale. La piattaforma può scalare a livello globale solo se è in grado di crescere mantenendo la sicurezza e l’utilità per tutti. Per questo motivo gli sviluppatori di Cardano hanno semplificato la loro metodologia, combinando una varietà di strumenti che vanno dai test basati sulla proprietà fino alle prove verificabili a macchina, per creare software ad alta garanzia anche in presenza di requisiti mutevoli.
Ricerca da codificare
La metodologia inizia con la ricerca scientifica. Ad oggi, IOHK ha pubblicato più di 60 articoli di ricerca che hanno contribuito a creare la piattaforma. Ogni articolo esamina un aspetto critico della tecnologia blockchain a partire dai primi principi. Come si ottiene il consenso in modo decentralizzato? Come si concepisce un contratto intelligente? Qual è la giusta struttura di ricompense per incentivare il buon comportamento? I ricercatori IOHK esaminano queste domande e presentano le loro risposte a riviste scientifiche e conferenze. Questi documenti contengono prove che devono superare una rigorosa revisione tra pari. Poi, per garantire che la qualità del nostro software renda giustizia alla scienza, viene sviluppata con metodi formali.
In sostanza, ciò significa che gli ingegneri di IOHK specificano ciò che il codice deve fare matematicamente. In questo modo, possono garantire che quando il codice viene eseguito, esso contenga le proprietà desiderate in esso progettate. Il codice è scritto in Haskell, un linguaggio di programmazione funzionale ad alta sicurezza con un sistema di tipo forte. Anche se Haskell è un ottimo strumento per implementare un software affidabile, non è infallibile, quindi il codice deve ancora essere testato. Un ottimo modo per scrivere i test è l’uso di QuickCheck, che permette agli sviluppatori di dichiarare le proprietà che dovrebbero essere sempre presenti in un programma. QuickCheck genera poi dei casi di test e cerca dei controcampioni minimi che violano quelle proprietà.
Nel codice che interagisce con il mondo esterno, in particolare con le applicazioni di rete, può essere difficile trovare controcampioni minimi. Questo perché l’ordine di esecuzione non è deterministico: può cambiare ogni volta che il software viene eseguito. Lo stesso codice può essere eseguito centinaia di volte e fallire una sola volta. Possiamo aggirare questo problema utilizzando simulazioni con ordine di esecuzione deterministico. L’esecuzione di test in simulazione ci permette di trovare e correggere in modo affidabile una classe di bug nei test, che altrimenti si verificherebbero solo casualmente in produzione.
Colmare il divario
Per avere un quadro della metodologia di sviluppo utilizzata per Cardano, consideriamo la metafora della costruzione di ponti. Quando un ingegnere civile costruisce un ponte, gran parte del suo tempo è passato dietro una scrivania. L’ingegnere civile pianifica un progetto, calcola la statica e ordina rilievi geografici. Durante questo periodo di tempo non succede nulla nel cantiere. Un osservatore non sarebbe in grado di vedere alcun progresso. Per la costruzione di ponti, questo è l’approccio corretto. Se la pianificazione non è accurata, è difficile e costoso correggere i problemi in una fase successiva. In definitiva, il risultato sarebbe un ponte costruito in ritardo ad un costo più alto, o che fallisce completamente. La mancanza di progressi visibili è un buon prezzo da pagare per un ponte funzionale e sicuro.
Quando si costruisce un software, apportare modifiche in fasi successive è molto più facile che nella costruzione. Questo è ciò che consente il comune approccio di sviluppo agile. Se uno sviluppatore agile costruisce un ponte, costruisce un pilastro in uno sprint rapido e poi il successivo in un secondo sprint. Il divario tra i pilastri sarebbe stato colmato in uno sprint finale e, se le cose non avessero retto, gli sviluppatori avrebbero aggiunto un altro sprint per risolvere eventuali problemi. Mentre i progressi sarebbero stati dimostrabili in cantiere, il prodotto finale avrebbe probabilmente avuto molti problemi. Questo crea un lavoro di pulizia alla fine del progetto che avrebbe potuto essere evitato con una migliore pianificazione in una fase precedente. Inoltre, il prodotto minimo realizzabile sarebbe stato probabilmente dato a un piccolo gruppo di persone per un test drive con l’aspettativa che non avrebbe funzionato per avvisare gli sviluppatori di bug. Inutile dire che è meglio che i ponti non siano progettati in questo modo.
Quando si sentono le parole “metodi formali”, molte persone nello sviluppo di software pensano all’approccio dell’ingegneria civile, che è soprannominato “cascata” e generalmente evitato. Si tratta di un malinteso comune ma sfortunato. Infatti, l’utilizzo di tecniche formali appropriate ci permette di avere la nostra torta, e anche di mangiarla: di avere un disegno complessivo (un disegno deliberato, non casuale, dovuto al montaggio di pezzi sviluppati in volata), di mostrare continuamente il progresso, e di mantenere la capacità di reagire al cambiamento delle esigenze.
Una tecnica chiave utilizzata dagli sviluppatori IOHK è quella delle specifiche eseguibili. Si tratta di progetti di alto livello, che astratto su dettagli di basso livello, scritti in un linguaggio che il computer può comprendere ed eseguire. Le specifiche eseguibili possono essere usate come prototipi per mostrare i progressi, ottenere un feedback dagli utenti e testare i presupposti. Oltre a ciò, i dettagli di livello inferiore possono essere aggiunti tramite successivi perfezionamenti. I nostri sviluppatori costruiscono il ponte per risolvere i problemi più grandi prima di tutto e poi aggiungono dei pilastri per rafforzarlo in un secondo momento. In un sistema software, i pilastri sarebbero caratteristiche come il salvataggio dei dati su disco, o l’utilizzo di algoritmi performanti, che sono necessari per un prodotto finale, ma che non sono essenziali per dimostrare la funzionalità complessiva.
Utilizzando specifiche eseguibili, si ottengono i vantaggi di una corretta pianificazione senza sacrificare la flessibilità. Gli sviluppatori di IOHK possono fissare l’aspetto del sistema su larga scala, e poi implementare i componenti adatti in base alle necessità. I test continui garantiscono che ogni componente si adatti al progetto complessivo. Questo aiuta a prevenire problemi che sono comuni in un approccio di integrazione tardiva. Con questa metodologia, otteniamo il meglio di entrambi i mondi: possiamo usare un design top-down (evitando problemi di integrazione tardiva, avendo sempre una buona gestione del design complessivo), e avere codice funzionante in anticipo (dimostrando i progressi, e consentendo test e feedback durante l’intero processo).
A prova di futuro
In definitiva, il metodo di costruzione dovrebbe essere determinato da ciò che si sta costruendo. IOHK sta costruendo un sistema operativo sociale e finanziario globale che richiede rigore e velocità. Formale contro agile è una falsa dicotomia. Invece, stiamo continuando a sviluppare la nostra metodologia che fonde il meglio di entrambi gli approcci: tecniche formali all’interno di un quadro di consegna agile, con un codice di garanzia più elevato e robusto su cui possiamo costruire per tutti i nostri futuri.
Traduzione a cura di LordWotton - se l’iniziativa ti è stata utile, considera l’opportunità di delegare i tuoi ADA ad una delle mie stakepool, VAULT o APEX 