Yuri Gurevich argues that algorithms are inherently deterministic and that probabilistic and quantum algorithms work by delegating non-algorithmic steps such as coin flips and quantum measurements to external oracles or assistants. He presents a theory of assisted algorithms with revised abstract state machine postulates, using a primality test and Grover's search as running examples.
This talk explores the history of high-assurance software, from the near-perfect code of the NASA Space Shuttle to the Airbus A320. It argues that while these rigorous engineering and formal verification practices were once too expensive for mainstream use, the economic shift brought by AI and agentic coding can make aerospace-level reliability a practical reality for a wide range of applications, solving the key quality limitations of current AI-generated code.