Buildings are built of stuff; programs are built of thoughts. That some information is more accessible because you have used it more recently is a fact about the brain rather than about software.
There you have, in a nutshell, the problem with software engineering as a formal discipline: its stubborn refusal to admit the above, in the face of determined pushes to do so from the likes of Bill Curtis (who’s been refused a Wikipedia entry because he’s less notable than any number of porn stars) or Jerry Weinberg.
Dijkstra’s view was that the limitations of the human mind are precisely the reason that software must be treated as mathematics and developed with mathematical rigour.
That depends on where the mathematics is done. Dijkstra’s and Hoare’s vision of programmers proving their own code correct with pencil and paper is unworkable. People cannot reliably do any sort of formal manipulation on paper, not even something as simple as making an exact copy of a document. The method can be exhibited on paper for toy examples, but everything works for toy examples. So what to do?
Compare the method of writing machine code by developing a method of translating a higher-level language into machine code. This can be exhibited on paper for toy examples, but of course that is only for didactic purposes, and one writes a compiling program to actually do that work in production. This reduces the work of writing programs in machine code to the task of writing just one program in machine code, the compiler, and by bootstrapping techniques that can be reduced even further. The amount of mathematics carried out on the human side of the interface is greatly reduced.
Similarly, proving things about programs has to be done automatically, or there’s no point. We have to prove things about programs, because computing hardware and software is mathematics, whether we wish it to be or not. Software engineering is precisely the problem of how human beings, who cannot reliably do mathematics, can reliably instruct a mathematical machine to do what we want it to with mathematical reliability.
I don’t have any solutions, it just seems to me that this is how to describe the problem. How do we interface thought-stuff with machine-stuff?
There you have, in a nutshell, the problem with software engineering as a formal discipline: its stubborn refusal to admit the above, in the face of determined pushes to do so from the likes of Bill Curtis (who’s been refused a Wikipedia entry because he’s less notable than any number of porn stars) or Jerry Weinberg.
Dijkstra’s view was that the limitations of the human mind are precisely the reason that software must be treated as mathematics and developed with mathematical rigour.
Note that this is the exact opposite of using the native architecture.
That depends on where the mathematics is done. Dijkstra’s and Hoare’s vision of programmers proving their own code correct with pencil and paper is unworkable. People cannot reliably do any sort of formal manipulation on paper, not even something as simple as making an exact copy of a document. The method can be exhibited on paper for toy examples, but everything works for toy examples. So what to do?
Compare the method of writing machine code by developing a method of translating a higher-level language into machine code. This can be exhibited on paper for toy examples, but of course that is only for didactic purposes, and one writes a compiling program to actually do that work in production. This reduces the work of writing programs in machine code to the task of writing just one program in machine code, the compiler, and by bootstrapping techniques that can be reduced even further. The amount of mathematics carried out on the human side of the interface is greatly reduced.
Similarly, proving things about programs has to be done automatically, or there’s no point. We have to prove things about programs, because computing hardware and software is mathematics, whether we wish it to be or not. Software engineering is precisely the problem of how human beings, who cannot reliably do mathematics, can reliably instruct a mathematical machine to do what we want it to with mathematical reliability.
I don’t have any solutions, it just seems to me that this is how to describe the problem. How do we interface thought-stuff with machine-stuff?