2025/02/02 by Angius, Nicola
#Epistemological Status of Computer Science #Filosofia dell'informatica #Fondamenti dell'informatica. #Foundations of Computer Science #Philosophy of Computer Science #Software Verification #Statuto epistemologico dell'informatica #Verifica software
paper · doi:10.13137/2036-9972/35928
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