Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Minds and Machines
Erschienen in: Minds and Machines 2/2011

01.05.2011

Program Verification and Functioning of Operative Computing Revisited: How about Mathematics Engineering?

verfasst von: Uri Pincas

Erschienen in: Minds and Machines | Ausgabe 2/2011

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

The issue of proper functioning of operative computing and the utility of program verification, both in general and of specific methods, has been discussed a lot. In many of those discussions, attempts have been made to take mathematics as a model of knowledge and certitude achieving, and accordingly infer about the suitable ways to handle computing. I shortly review three approaches to the subject, and then take a stance by considering social factors which affect the epistemic status of both mathematics and computing. I use the analogy between mathematics and computing in reverse—that is to say, I consider operative computing as a form of making mathematics, and so attempt to learn from computing to mathematics in general. I conclude that “mathematics engineering” is a field to be both developed for practical improvement of doing mathematics and taken into consideration while philosophizing about mathematics as well.
Vorheriger Artikel Scientific Theories of Computational Systems in Model Checking

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Fußnoten
1
The word "operational" ("operative", "operating", etc') is somewhat overloaded in computer science (operating systems, operative research, and more), but it is still used in this work, mostly with "computing", referring to "practical computing", in the sense of actual programs run on electronic machines. Sometimes it is used for activities being taken in some other, probably more theoretical and general, context.
 
2
The term 'software engineering' was coined, apparently, around the middle of 1969, before the organization of the first conference of software engineering in October 1969 (See Pelaez 1988). As we are interested here in "engineering" of different aspects, not only of software, the term 'computing engineering' might be preferable, though mostly we use 'software engineering', for reasons of tradition.
 
3
Some crucial developments in (what is considered nowadays as) the theory of computer sciences, which has partly evolved prior to operational electronic computing, have been done as mathematical works in the full sense of the word. Here we consider latter developments of operational computing—particularly actual programming, design and creation of programming tools, running computer programs and operating computer systems.
 
4
Of course, this distinction is kind of similar to the well-known distinction in philosophy between the "a priori" and the "a posteriori" knowledge. (See also footnote 10 here.) In a later interview Fetzer said that such a distinction had been, indeed, in his mind, but he had chosen not to use these terms, considering them as too technical a philosophical terminology (see (MacKenzie 2001, p. 215)). Fetzer also distinguishes more delicately between statements which are learnt directly by observation and those which are deduced by induction and causality, but the important distinction here is the one described before.
 
5
For an updated list of publications, see, e.g., (Rapaport 2007) (up to 12 April 2007, and occasionally updated).
 
6
Very many texts of the philosophical literature deal with variety of aspects of this reach subject. See, e.g., the comprehensive and systematic (Hersh 1997; Shapiro 2000).
 
7
There are different kinds of "realistic" views in the philosophy of mathematics (as well as in philosophy in general). One view is taking mathematical objects to be existing independently of the human mind, so having their properties independently of our being in touch with those objects ("ontological realism"). Here we make do with a more moderate version of realism, assuming the truth value of mathematical statements is determined independently of the human mind ("truth-value realism") (see, e.g., (Shapiro 2000)). Of course, the first kind implies the second one.
 
8
Arguments of this kind can be found in texts of philosophy of mathematics, such as, e.g., (Davis 1972; Ernest 1991; Bloor 1994; Hersh 1997).
 
9
An interesting discussion of such situations, from a philosophical point of view, appears on (Tymoczko 1979).
 
10
Here we use the well-known terms "analytic"/"synthetic", as our representation here fits that duo, at least in many of its common uses in philosophy, more than the aforementioned in footnote 4, "a priori"/"a posteriori". The relations between these two duos and the differences in meaning between them are a complicated and much-discussed philosophical issue, which we do not need to dwell on here. The terms are used mainly as "keyword connectors" to the relevant philosophical discussions.
 
11
The philosophical literature considering this issue is very rich. A few works to mention, of the very many, are the momentous and much celebrated, (Quine 1951), its important "philosophical descendents", (Putnam 1962) and (Pigden 1987), and the latter work, (Putnam 2002).
 
12
That issue is also treated in many works. See, e.g., (Kitcher 1984; Crowe 1988; Sasaki 2005).
 
13
Every programmer knows the process of debugged interpreting—a controlled executing in steps of a computer program, inspecting and checking the result of every step, comparing it with the desired and expected result of that step.
 
14
Scherlis and Scott, considering the issue of program verification, have probably had some similar idea in mind, writing, in their interesting work, (Scherlis and Scott 1983): "But, even relatively elementary programs tend to be more complicated than elementary theorems. Why? Because in a certain sense more of their structure has to be made more explicit. In mathematical literature, it is often sufficient to do one precise calculation, and for the other cases say 'similarly'. A proof is often more a genteel tourist guide than instructions for a treasure hunt. Programs, on the other hand, not only operate on very highly structured data, but they must do so in unobvious ways in order to be efficient."
 
15
See the aforementioned in the previous footnote, (Scherlis and Scott 1983).
 
16
Computing errors do happen, as said, and so faults of computing system are not rare at all. But here we consider "disasters" as faults which result in harsh damage, such as death, severe injury, or grave financial loss. Such cases are very uncommon. See, e.g., (MacKenzie 2001, pp. 299–301; TRD 2009).
 
17
For interesting suggestions and discussions of such explanations, see (Collins 1990, pp. 62–65; MacKenzie 2001, Chap. 9).
 
Literatur
Asperti, A., Geuvers, H., & Natarajan, R. (2009). Social processes, program verification and all that. Mathematical Structures in Computer Science, 19(5), 877–896.MathSciNetMATHCrossRef
Auslander, J. (2008). On the roles of proof in mathematics. In B. Gold & R. A. Simons (Eds.), Proof and other dilemmas: Mathematics and philosophy (pp. 61–77). Washington: Mathematical Association of America.
Bjørner, D. (2006). Software engineering 1: Abstraction and modelling. An EATCS Series. Berlin: Springer.
Bloor, D. (1994). What can the sociologist of knowledge say about 2 + 2=4? In P. Ernest (Ed.), Mathematics, education and philosophy: An international perspective (pp. 15–26). London: Falmer Press.
Cockburn, A. (2004). The end of software engineering and the start of economic-cooperative gaming. Computer Science and Information System, 1(1), 1–32.CrossRef
Colburn, T. R., Fetzer, J. H., & Rankin, T. L. (Eds.). (1993). Program verification: Fundamental issues in computer science. Dordrecht: Kluwer Academic Publishers.MATH
Collins, H. (1990). Artificial experts: Social knowledge and intelligent machines. Cambridge: Cambridge University Press.
Crowe, M. J. (1988). Ten misconceptions about mathematics and its history. In W. Aspray & P. Kitcher (Eds.), History and philosophy of modern mathematics (pp. 260–277). Minneapolis: University of Minnesota Press.
Davis, P. J. (1972). Fidelity in mathematical discourse: Is one and one really two? American Mathematical Monthly, 79(3), 252–263.MathSciNetMATHCrossRef
De Millo, R. A., Lipton, R. J., & Perlis, A. J. (1979). Social processes and proofs of theorems and programs. Communications of the ACM, 22(5), 271–280.CrossRef
Detlefsen, M. (Ed.). (1992). Proof and knowledge in mathematics. London: Routledge.MATH
Ernest, P. (1991). The philosophy of mathematics education. London: Falmer Press.
Fetzer, J. H. (1988). Program verification: The very idea. Communications of the ACM, 31(9), 1048–1063.CrossRef
Giaquinto, M. (2005). Mathematical activity. In P. Mancosu, K. F. Jorgensen, & S. A. Pedersen (Eds.), Visualization explanation and reasoning styles in mathematics (pp. 75–87). Dordrecht: Springer.CrossRef
Harel, D. (with Feldman Y.) (2004). Algorithmics: The spirit of computing, 3rd ed. Reading: Addison-Wesley.
Hersh, R. (1997). What is mathematics, really? Oxford: Oxford University Press.
Hoare, C. A. R. (1969). An axiomatic basis for computer programming. Communications of the ACM 12(10), 576–580, 583.
Hoare, C. A. R. (1986). Mathematics of Programming. BYTE (August). Reprinted in Colburn, T. R., Fetzer, J. H., & Rankin, T. L. (Eds.) (1993) (pp. 135–154).
Kitcher, P. (1984). The nature of mathematical knowledge. Oxford: Oxford University Press.
Liskov, B., & Zilles, S. (1977). An introduction to formal specifications of data abstractions. In R. T. Yeh (Ed.), Current trends in programming methodology (pp. 1–32). Englewood Cliffs: Prentice Hall.
MacKenzie, D. (2001). Mechanizing proof: Computing, risk, and trust. Cambridge: Cambridge University Press.MATH
MacKenzie, D. (2005). What in the name of Euclid is going on here? Science, 207(5714), 1402–1403.MathSciNet
Mancosu, P. (2000). On mathematical explanation. In E. Grosholtz & H. Berger (Eds.), Growth of mathematical knowledge (pp. 103–120). Dordrecht: Kluwer Academic Publishers.
Maurer, W. D. (1979). Letter to the editor. Communications of the ACM, 22, 625–629.
Pelaez, E. (1988). A Gift from Pandora’s Box: The Software Crisis. Ph.D. dissertation. Edinburgh: University of Edinburgh.
Putnam, H. (1962). It Ain’t necessarily so. Journal of Philosophy, 59, 658–671.CrossRef
Putnam, H. (2002). The collapse of the fact/value dichotomy. Cambridge: Cambridge University Press.
Quine, W. V. O. (1951). Two dogmas of empiricism. Philosophical Review, 60, 20–43.CrossRef
Resnik, M., & Kushner, D. (1987). Explanation, independence and realism in mathematics. British Journal for the Philosophy of Science, 38, 141–158.MathSciNetMATHCrossRef
Sandborg, D. (1998). Mathematical explanation and the theory of why-questions. British Journal for the Philosophy of Science, 49, 603–624.MathSciNetMATHCrossRef
Schach, S. R. (2007). Algorithmics: Object-oriented and classical software engineering (7th ed.). New York: McGraw-Hill.
Scherlis, W. L., & Scott, D. S. (1983). First steps towards inferential programming. In R. E. A. Mason (Ed.), Information processing 83 (pp. 199–212). Amsterdam: Elsevier Science Publishers.
Shapiro, S. (2000). Thinking about mathematics: The philosophy of mathematics. Oxford: Oxford University Press.MATH
Simons, C. L., Parmee, I. C., & Coward, P. D. (2003). 35 years on: To What extent has software engineering design achieved its goals? IEE Proceedings–Software, 19(5), 337–350.
Smith, B. C. (1985). Limits of correctness in computers. As center for the study of language and information report No. CSLI-85–36. Stanford: Ventura Hall.
Tymoczko, T. (1979). The four-color problem and its philosophical significance. Journal of Philosophy, 76, 57–83.CrossRef
Zemanek, H. (1979). Abstract architecture. In D. Bjørner (Ed.), Abstract software specifications (pp. 1–42). Copenhagen: Springer.
Metadaten
Titel
Program Verification and Functioning of Operative Computing Revisited: How about Mathematics Engineering?
verfasst von
Uri Pincas
Publikationsdatum
01.05.2011
Verlag
Springer Netherlands
Erschienen in
Minds and Machines / Ausgabe 2/2011
Print ISSN: 0924-6495
Elektronische ISSN: 1572-8641
DOI
https://doi.org/10.1007/s11023-011-9237-z

Weitere Artikel der Ausgabe 2/2011

Minds and Machines 2/2011 Zur Ausgabe

OriginalPaper

Problems for a Philosophy of Software Engineering

OriginalPaper

Specification

OriginalPaper

Do Accelerating Turing Machines Compute the Uncomputable?

OriginalPaper

Scientific Theories of Computational Systems in Model Checking

OriginalPaper

Descartes Among the Robots

OriginalPaper

Sense and Reference on the Web

Premium Partner

    Bildnachweise