Comment by Mikhail_Edoshin
6 days ago
Programming is very similar to inductive reasoning, you establish some facts, do a step that changes something, and establish facts after the step and then repeat that with different steps until you get the facts you are after. (See e.g. Manber's book.) If you merely set out to rigorously write the computation steps, the result will already be a proof sufficient for a human. I am not sure, but I think Dijkstra ended up doing or maybe just writing about something like that, he wanted to get programs that were correct by construction, not proven to be correct afterwards.
What is utterly lacking is a formal notation for these computation-reasoning steps that is not tied to a specific programming language. As a result what we get now is an informal specifications and a bunch of different final implementations for different languages. Whatever knowledge could be kept is not kept in any organized way.
I wasn't familiar with that book. For other users, I think the book they are referring to is Introduction to Algorithms A Creative Approach by Udi Manber.
> What is utterly lacking is a formal notation for these computation-reasoning steps that is not tied to a specific programming language
A formal notation for this is a programming language. Which is why everyone use pseudo code or something equivalent for a first pass thinking or for communication.
Not quite. It is in a way (very visible when we talk about invariants), but it is not, well, semantic. A good notation for those steps would allow me to make only the distinctions I care for and ignore the distinctions I do not care for. So, for example, if I want to describe the greatest common divisor algorithm, I would only focus on the arithmetic part and define the domain of the parameters as "positive integers" (or maybe "non-negative integers").
A real programming language has a different goal: the code must run and do something useful. So I am unlikely to be able to define the domain like that (won't be able to make important distinctions) and, at the same time, will likely have to attend to things I do not care about (will have to make unimportant distinctions). All this will cripple and obscure the logic. This is what happens now and as a result we have a different implementation of everything for every programming language.