> 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.