3 ms·

Computers are formal systems as much as an alternating electrical current is a complex number, same with programming languages, even though both programming lan

by stiff 12y ago

Computers are formal systems as much as an alternating electrical current is a complex number, same with programming languages, even though both programming languages and formal systems can be viewed as abstract entities. Technically speaking all that can be said is that certain programming languages can be models for certain formal systems, and there is a big difference between being a model for a formal theory and something simply being only a formal theory: http://en.wikipedia.org/wiki/Reification_%28fallacy%29 http://en.wikipedia.org/wiki/Reification_%28fallacy%29 Programming language designers of most popular programming languages have no clue about neither denotational nor operational semantics and make use of no formal theory whatsoever. Anyhow, I do not deny the importance of various kinds of mathematics for programming, in some selected places and in the sense of writing programs that do mathematics. I am saying two things: - The attempts so far to turn programming itself into a single mathematical theory have failed miserably. Can you name one really important algorithm that was discovered by doing derivations in a formal axiomatic theory of programming? There is the "Algebra of programming" theory by Bird, the "Elements of programming" by Stepanov, but nothing particularly striking seems to ever come out of it, only proofs of things we already know. - There are hundreds of aspects of programming that have nothing to do with mathematics and turned out to be of far bigger importance than finding effective means of formal correctness proofs of programs. To give one example, programmers have to work in teams with the size of problems we are dealing with today, something the formal methods people never seemed to address much, and issues with communication and coordination cause much more problems than simple logical errors in algorithms.

loup-vaillant 12y ago
> Programming language designers of most popular programming languages have no clue about neither denotational nor operational semantics and make use of no formal theory whatsoever. That may explain why so many of our popular languages have several glaring flaws. Java doesn't support tail calls dammit! We had to wait for scheme to finally have lexical scope! C++ is impossible to parse! > The attempts so far to turn programming itself into a single mathematical theory have failed miserably. Wait, what attempts? I've read many Haskell papers, and did not stumble upon such a thing.
- stiff 12y ago
  I have specifically mentioned two such attempts.
  - loup-vaillant 12y ago
    Okay. Though if it's not a peer reviewed paper, it doesn't exist. Anyway, I have a more positive outlook: those "failures" are just the beginning. We'll build on those. We failed to fly for a long time, for instance.
    - stiff 12y ago
      There are lots of papers, dating back to the 1970s: http://www.cs.ox.ac.uk/activities/publications/date/algprog.html http://www.cs.ox.ac.uk/activities/publications/date/algprog.... Actually Dijkstra also was a proponent of deriving programs, it's discussed in his "Discipline of programming" and 30 years ago there was some interest in this, with lots of papers published, but it never gained much traction: http://en.wikipedia.org/wiki/Program_derivation http://en.wikipedia.org/wiki/Program_derivation
- nnq 12y ago
  > C++ is impossible to parse! Bold, claim, considering all the C++ parsers out there that work just fine... The fact that you need to code a parser by hand doesn't mean that the language is impossible to parse at all. And even for an easier to parse language, if you want to write a parser that spits error messages that make any sense to most users, and that may use some heuristics to guess the programmer's intend in order to give even better error messages, you will have to code it by hand anyway.

by stiff 12y ago

loup-vaillant 12y ago

> Programming language designers of most popular programming languages have no clue about neither denotational nor operational semantics and make use of no formal theory whatsoever. That may explain why so many of our popular languages have several glaring flaws. Java doesn't support tail calls dammit! We had to wait for scheme to finally have lexical scope! C++ is impossible to parse! > The attempts so far to turn programming itself into a single mathematical theory have failed miserably. Wait, what attempts? I've read many Haskell papers, and did not stumble upon such a thing.

stiff 12y ago
I have specifically mentioned two such attempts.
- loup-vaillant 12y ago
  Okay. Though if it's not a peer reviewed paper, it doesn't exist. Anyway, I have a more positive outlook: those "failures" are just the beginning. We'll build on those. We failed to fly for a long time, for instance.
  - stiff 12y ago
    There are lots of papers, dating back to the 1970s: http://www.cs.ox.ac.uk/activities/publications/date/algprog.html http://www.cs.ox.ac.uk/activities/publications/date/algprog.... Actually Dijkstra also was a proponent of deriving programs, it's discussed in his "Discipline of programming" and 30 years ago there was some interest in this, with lots of papers published, but it never gained much traction: http://en.wikipedia.org/wiki/Program_derivation http://en.wikipedia.org/wiki/Program_derivation
nnq 12y ago
> C++ is impossible to parse! Bold, claim, considering all the C++ parsers out there that work just fine... The fact that you need to code a parser by hand doesn't mean that the language is impossible to parse at all. And even for an easier to parse language, if you want to write a parser that spits error messages that make any sense to most users, and that may use some heuristics to guess the programmer's intend in order to give even better error messages, you will have to code it by hand anyway.