211service.com
Codice garantito
Ariel Davis
Adam Chlipala, professore associato di informatica al MIT, pensa che ci sia un modo migliore per scrivere programmi per computer.
La maggior parte dei programmi elenca solo le operazioni che il computer dovrebbe eseguire quando riceve particolari tipi di dati. Il programmatore deve scrivere dei test per determinare se un programma fa ciò che dovrebbe e poiché è praticamente impossibile prevedere tutti i modi in cui un programma potrebbe essere utilizzato, la maggior parte dei software presenta dei bug.
Chlipala preferisce la cosiddetta programmazione funzionale. Invece di mettere insieme comandi imperativi, un programmatore funzionale definisce un insieme di funzioni o relazioni matematiche tra input e output. In sostanza, la programmazione funzionale esprime ciò che fa un programma come un insieme di equazioni.
Pensare ai programmi come a combinazioni di funzioni può non essere intuitivo, ma per le persone per cui funziona è davvero un incredibile potenziatore della produttività, afferma Chlipala. Per prima cosa, può eliminare i test. I programmi funzionali sono così matematicamente precisi che è relativamente semplice verificarli o dimostrare che fanno ciò che dovrebbero, automaticamente.
Uno di Chlipala principali interessi di ricerca sta ampliando il campo di applicazione della verifica automatica. Ad esempio, gli strumenti di verifica sviluppati da lui e dai suoi colleghi hanno permesso di creare il primo file system, la parte di un sistema operativo che governa l'archiviazione dei dati, garantendo di non perdere i dati del programma durante un arresto anomalo del sistema.
Un altro vantaggio dei linguaggi funzionali è che eliminano gran parte del lavoro grugnito dalla programmazione. Ancora una volta, poiché i programmi funzionali sono così precisi, è facile per i compilatori, i programmi che trasformano il codice in file eseguibili, capire come farli funzionare in modo più efficiente.
Uno degli strumenti più popolari di Chlipala è un linguaggio funzionale chiamato Ur/Web, l'unico linguaggio di programmazione che consente ai programmatori di specificare tutte le funzionalità di un'applicazione Web in un unico programma. Il compilatore di Ur/Web genera quindi automaticamente il codice XML, il codice JavaScript e le query del database necessarie per implementare l'applicazione. Garantisce inoltre che questi diversi componenti interagiscano correttamente.
Ur/Web è simile ad altri linguaggi funzionali, ma aggiunge funzionalità di sicurezza che gli consentono di tappare automaticamente i buchi comuni nelle applicazioni Web. Ad esempio, può garantire che una parte del suo codice importato in una sezione di una pagina (come un annuncio pubblicitario) non possa spiarne un'altra (come uno strumento di calendario).
Come molti scienziati informatici sulla trentina, Chlipala si era cimentato nella scrittura di videogiochi al liceo. Ma quell'impresa lo portò rapidamente in una direzione diversa. Quando era una matricola, i suoi tentativi di scrivere giochi per la calcolatrice grafica di Texas Instruments lo hanno portato a sviluppare un compilatore per il dispositivo.
Ha continuato a concentrarsi sui compilatori come studente universitario alla Carnegie Mellon University, e nel suo primo semestre come studente laureato presso l'Università della California, Berkeley, il suo futuro relatore di tesi gli ha chiesto se gli sarebbe piaciuto contribuire a un progetto sul computer- verifica assistita. Chlipala è stata subito catturata.
C'è un certo tipo di personalità paranoica che diventa dipendente da questo tipo di lavoro, e quello sono sicuramente io, dice. Non ci sono molte cose che sono assolutamente sicure in questo mondo, ma quando esegui prove automatiche sui programmi, ti avvicini abbastanza.