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.