Utente:Luigi Pignataro 98/Sandbox
METODOLOGIA DELL' INFORMATICA
La scienza e la filosofia sono distinte dal fatto che la scienza cerca una spiegazione mentre la filosofia cerca la giustificazione. Chiedere che cosa sia il cervello, ad esempio, è una questione scientifica, mentre chiedere che una rete neurale artificialmente costruita sia conscia è filosofica. Quindi la filosofia è stata caratterizzata come la valutazione critica delle credenze attraverso l'analisi dei concetti in una determinata area di indagine. Naturalmente, la scienza si occupa anche di analizzare i concetti. Nel cercare spiegazioni, essa spesso costruisce modelli per testare ipotesi e spiegare i fenomeni. Questi modelli, sotto forma di apparato sperimentale, sono ovviamente oggetti fisici. Essi costruiti e manipolati nell'informatica, tuttavia, non sono affatto fisici. Scienza del computer è una scienza che si occupa dello studio dei processi computazionali. Un processo computazionale si distingue, per esempio, da un processo chimico o elettrico, in quanto viene studiato in modi che ignorano la sua natura fisica. Ad esempio, il processo mediante il quale un giocatore di carte dispone le carte nella sua mano, e il processo attraverso il quale un computer ordina i nomi in un elenco clienti, sebbene non condividano nulla in comune fisicamente, può tuttavia incorporare lo stesso processo computazionale. Ad esempio, possono entrambi procedere con la scansione degli elementi da disporre uno per uno, determinando la posizione corretta di ciascun elemento scansionato relativamente agli elementi già letti e inserendoli in quel luogo, forse rendendo necessario lo spostamento di elementi precedentemente scansionati per creare spazio . Questo modello può essere testato, in modo analogo ad un'ipotesi che viene testata nelle scienze naturali, eseguendo il programma e osservandone il comportamento. Costruire modelli di calcolo e rispondere a questo tipo di domande formano una parte importante di ciò che fanno gli scienziati informatici. La crescita esplosiva del numero di applicazioni negli ultimi decenni ha dimostrato che non vi è alcun limite al numero di processi suscettibili ad una modellazione tramite computer. Non solo le attività tradizionali, come la tenuta dei registri, gli investimenti, le pubblicazioni e le operazioni bancarie, sono state semplicemente convertite in controllo tramite modelli computazionali, ma sono stati creati tipi completamente nuovi di attività che non sarebbero stati possibili senza tali modelli. Queste sono le "virtuali" attività familiari descritte nella lingua del cyberspazio: e-mail, chat room, web fi ng, shopping online, giochi su Internet e così via. Il ruolo della filosofia in quel sottosistema dell'informatica noto come intelligenza artificiale è stato riconosciuto da tempo, dato il ruolo del ragionamento nell'IA. E il contrario, il ruolo dell'IA in filosofia, è stato anche messo in evidenza da alcuni, anche se controverso. Quindi, un ruolo perfetto della filosofia è quello di tentare di collocare l'informatica nell'ampio spettro di ricerca che costituisce la scienza. La filosofia dovrebbe affrontare domande come: Qual è la relazione tra matematica e informatica? C'è un senso in cui l'informatica è scienza sperimentale? Un programmatore di computer è semplicemente un mago dei dati o può anche dedicarsi alla modellazione delle informazioni? Dal punto di vista della metodologia dell'informatica, la più problematica di queste domande riguarda la relazione tra matematica e computer la scienza e la natura dell'astrazione nell'informatica.
I contributi filosofici ai fondamenti delle discipline scientifiche si concentrano spesso intorno a "questioni cardine" riguardanti i tentativi di riduzione. Nella filosofia della biologia, per esempio, la domanda è se le leggi biologiche possono essere tradotte in leggi fisiche. Una prima "questione centrale" nella filosofia dell'informatica è se la scienza dei computer può essere ridotta a un ramo della matematica. Il modo in cui un informatico risponde a questa domanda può influenzare molto la sua metodologia. La gamma di prospettive da cui il problema del riduzionismo può essere affrontato è ampia. Considera la seguente opinione, espressa da Hoare: "I programmi per computer sono espressioni matematiche. Descrivono, con precisione senza precedenti e nei minimi dettagli, il comportamento, intenzionale o non voluto, del computer sul quale sono eseguiti "(Hoare 1986: 115). E questa alternativa, offerta da C. Floyd: "I programmi sono strumenti o ambienti di lavoro per le persone. Sono progettati in processi di apprendimento e comunicazione per soddisfare i bisogni umani "(Floyd 1987: 196). La visione espressa da Hoare è inequivocabile: i programmi per computer sono espressioni matematiche. La citazione di Floyd è meno precisa, ma esprime una visione della funzione dei programmi per l'uomo in termini decisamente non matematici. Sebbene queste visioni non siano necessariamente in contraddizione tra loro, possono sicuramente segnalare interpretazioni contrastanti su come i programmi di computer dovrebbero essere progettati, costruiti e usati. L'uso della verifica formale nell'informatica ha generato un dibattito sin dall'apparizione di un documento sulla verifiche sui processi sociali di R. DeMillo, R. Lipton e A. Perlis nel 1979. Ma non è stato fino al 1988 che queste domande hanno attirato l'attenzione di un filosofo "puro", quando J. Fetzer resuscitò il programma di verifica / dibattito sui processi sociali di un decennio prima e lo sottopose a una vera analisi filosofica. Prima di allora, il dibattito sulle questioni era evidenziato principalmente dalle differenze nei resoconti visionari di come la giovane disciplina dell'informatica dovrebbe procedere, data non dai filosofi ma dai professionisti e insegnanti di informatica. Uno dei primi fautori della verifiche formali è stato John McCarthy, negli anni '50. Egli era originariamente motivato da una teoria del calcolo che avrebbe consentito, tra gli altri vantaggi, la traduzione automatica da un paradigma linguistico a un altro. Ora, dopo quasi 30 anni, si può guardare indietro e confermare la traduzione automatica del programma, con l'aiuto di precise specificazioni linguistiche, è stato realizzato nel caso di compilatori di linguaggi. Questi sono strumenti di programmazione che trasformano programmi scritti in linguaggi umani familiari come Java, nel linguaggio macchina dei computer, che è composto solo da zero e uno. Tuttavia, come dimostra la dichiarazione di non responsabilità della garanzia del manuale di riferimento di ogni lingua, nessun compilatore automatico in tutti i casi traduce correttamente i programmi nella lingua della macchina. Quindi, vi è la distinzione tra (1) l'uso di metodi matematici durante la traduzione del linguaggio per produrre codice di linguaggio macchina altamente affidabile, e (2) usando metodi matematici per dimostrare che un programma sorgente si comporterebbe, in senso astratto, esattamente come la sua specificazione implica . McCarthy, non vedendo alcun ostacolo a (2), scrisse: la prova dovrebbe essere controllata da un programma per computer. (McCarthy 1962: 22).Fetzer ha sostenuto che la presenza o l'assenza di processi sociali è, per esempio, la noia e la mancanza di glamour coinvolti nella revisione delle prove prodotte dai veri verificatori meccanici. Ma per Fetzer, se questo è tutto ciò che c'è da criticare sulla verifica formale, non è sostanziale. Come sottolineato da Fetzer, i processi sociali sono caratterizzati da modelli transitori di comportamento umano che, si potrebbe immaginare, in diverse circostanze riserverebbero per la verifica del programma lo stesso tipo di eccitazione e collaborazione collegiale che segna la migliore ricerca matematica. Fetzer credeva che la programmazione formale non possa adempiere al ruolo che alcuni dei suoi sostenitori gli assegnano nell'ingegneria del software, ma la attacca da una prospettiva non sociale, più strettamente filosofica. Ciò ha a che fare con la relazione tra modelli matematici e sistemi causali che intendono descrivere. L'esame accurato di questa relazione rivela, per Fetzer, la natura relativa, piuttosto che assoluta, della correttezza del programma che garantisce la verifica formale. È solo possibile provare formalmente qualcosa riguardo a un modello formale, cioè un modello formale di programma pronunciato nel testo formale. Non è possibile dimostrare concretamente qualcosa su un modello causale, cioè un programma in esecuzione, rappresentato in un substrato fisico ed elettronico di processore bistabile e elementi di memoria. Le forti affermazioni dei verificatori formali sono vittime di questa ambiguità perché ignorano diverse distinzioni: tra i programmi in corso su macchine astratte senza controparti fisiche e programmi che funzionano su macchine astratte con una controparte fisica; tra "programmi-testi" e "programmi-come-cause"; e tra matematica pura e applicata. Riconoscendo queste distinzioni, per Fetzer, rivela che l'affermazione che è possibile ragionare in modo puramente aprioristico sul comportamento di un programma è vera se il comportamento è puramente astratto; falso, e pericolosamente fuorviante altrimenti. Ciò garantisce l'indispensabilità dei metodi empirici nel processo di sviluppo del software, ad esempio l'uso del test del programma per eliminare i bug del programma.