Search

This paper sheds light on the shift that is taking place from the practice of 'coding', namely developing programs as conventional in the software community, to the practice of 'curing', an activity that has emerged in the last few years in Deep Learning (DL) and that amounts to curing the data regime to which a DL model is exposed during training. Initially, the curing paradigm is illustrated by means of a study-case on autonomous vehicles. Subsequently, the shift from coding to curing is analysed taking into consideration the epistemological notions, central in the philosophy of computer science, of function, implementation, and correctness. First, it is illustrated how, in the curing paradigm, the functions performed by the trained model depend much more on dataset curation rather than on the model algorithms which, in contrast with the coding paradigm, do not comply with requested specifications. Second, it is highlighted how DL models cannot be considered implementations according to any of the available definitions of implementation that follow an intentional theory of functions. Finally, it is argued that DL models cannot be evaluated in terms of their correctness but rather in their experimental computational validity., Author(s): Nicola Angius [sup.1], Alessio Plebe [sup.1] Author Affiliations: (1) grid.10438.3e, 0000 0001 2178 8421, Department of Cognitive Science, University of Messina, , Messina, Italy Introduction Let us loosely use [...]

This paper provides a review of Raymond Turner's book Computational Artefacts. Towards a Philosophy of Computer Science. Focus is made on the definition of program correctness as the twofold problem of evaluating whether both the symbolic program and the physical implementation satisfy a set of specifications. The review stresses how these are not two separate problems. First, it is highlighted how formal proofs of correctness need to rely on the analysis of physical computational processes. Secondly, it is underlined how software testing requires considering the formal relations holding between the specifications and the symbolic program. Such a mutual dependency between formal and empirical program verification methods is finally shown to influence the debate on the epistemological status of computer science., Author(s): Nicola Angius [sup.1] Author Affiliations: (1) grid.11450.31, 0000 0001 2097 9138, Department of History, Human Sciences, and Education, University of Sassari, , Sassari, Italy Raymond Turner's book Computational Artefacts. [...]

I critically review Raymond Turner's Computational Artifacts - Towards a Philosophy of Computer Science by placing beside his position a rather different one, according to which computer science is a branch of, and is therefore subsumed by, immaterial formal logic., Author(s): Selmer Bringsjord [sup.1] [sup.2] [sup.3] [sup.4] Author Affiliations: (1) grid.33647.35, 0000 0001 2160 9198, Rensselaer AI & Reasoning (RAIR) Laboratory, Rensselaer Polytechnic Institute (RPI), , 12180, Troy, NY, USA [...]

Turner (2018 (See CR52)) argues that computer programs must have purposes, that implementation is not a kind of semantics, and that computers might need to understand what they do. I respectfully disagree: Computer programs need not have purposes, implementation is a kind of semantic interpretation, and neither human computers nor computing machines need to understand what they do., Author(s): William J. Rapaport [sup.1] [sup.2] [sup.3] [sup.4] Author Affiliations: (1) grid.273335.3, 0000 0004 1936 9887, Department of Computer Science and Engineering, University at Buffalo - The State University of [...]

One might poetically muse that computers have the essence both of logic and machines. Through the case of the history of Separation Logic, we explore how this assertion is more than idle poetry. Separation Logic works because it merges the software engineer's conceptual model of a program's manipulation of computer memory with the logical model that interprets what sentences in the logic are true, and because it has a proof theory which aids in the crucial problem of scaling the reasoning task. Scalability is a central problem, and some would even say the central problem, in appli- cations of logic in computer science. Separation Logic is an interesting case because of its widespread success in verification tools. For these two senses of model-the engineering/conceptual and the logical-to merge in a genuine sense, each must maintain their norms of use from their home disciplines. When this occurs, both the logic and engineering benefit greatly. Seeking this intersection of two different senses of model provides a strategy for how computer scientists and logicians may be successful. Furthermore, the history of Separation Logic for analysing programs provides a novel case for philosophers of science of how software engineers and computer scientists develop models and the components of such models. We provide three contributions: an exploration of the extent of models merging that is necessary for success in computer science; an introduction to the technical details of Separation Logic, which can be used for reasoning about other exhaustible resources; and an introduction to (a subset of) the problems, process, and results of computer scientists for those outside the field., Author(s): David Pym [sup.1] , Jonathan M. Spring [sup.1] , Peter O'Hearn [sup.1] Author Affiliations: (Aff1) 0000000121901201, grid.83440.3b, Computer Science, University College London, , Gower Street, WC1E 6BT, London, UK [...]