Abstract
This paper examines one central problem in the philosophy of computer science, namely the question of whether computer programs can be verified by means of a mathematical proof. Firstly, program verification is defined and the classical debate on its feasibility is recalled under the light of a dual ontology of computational systems. Secondly, the current resurgence of the debate is analysed underlining its logical, technological, and philosophical motivations. Finally, it is shown how adopting a stratified ontology for computational systems one may recombine the different positions in the debate, arguing how program verification involves both deductive and inductive reasoning.
Questo articolo esamina il problema, centrale in filosofia dell’informatica, inerente la possibilità di verificare i programmi per calcolatore mediante una dimostrazione matematica. In primo luogo, viene definita la verifica software e viene ricordato il dibattito classico sulla sua possibilità alla luce di una ontologia dualistica dei sistemi computazionali. In secondo luogo, viene analizzato il dibattito attuale sottolineando le motivazioni logiche, tecnologiche e filosofiche del suo rinnovato interesse. Infine, viene mostrato come, adottando un’ontologia stratificata per i sistemi computazionali, si possano ricombinare le diverse posizioni nel dibattito, sostenendo come la verifica software richieda tanto il ragionamento deduttivo quanto quello induttivo.
Citazione
Nicola Angius, “Can Computer Programs be Formally Verified?”, in “APhEx 28”, 2023, pp.
Numero delle rivista
Visualizza e scarica il file PDF
Vai agli indici
AUTORI&AUTRICI
È ricercatore in Logica e Filosofia della Scienza presso il Dipartimento di Scienze Cognitive, Psicologiche, Pedagogiche e degli studi culturali dell'Università degli Studi di Messina, presso il quale insegna Filosofia della Scienza, Epistemologia della Psicologia e Philosophy of Computing. I suoi interessi di ricerca vertono sull'epistemologia dell'informatica con applicazioni nel campo dell'intelligenza artificiale e delle scienze cognitive. È co-autore della voce "Philosophy of Computer Science" per la Stanford Encyclopedia of Philosophy".