4 ms·

Nice post. Can you clarify your last sentence? What do you mean by "preference for operational reasoning"? What's an example of the more effective methods fo

• catnaroek 11y ago
  “Operational reasoning” means using execution traces (the sequence of states underwent by a process under the control of your program) to derive conclusions about the program. You can do it in your head, using a piece of paper, using a debugger, using strategic assertions, etc. By “more effective methods for reasoning about programs at scale”, what I mean is analyzing the program in its own right, without reference to specific execution traces. There are several kinds of program analyses that can be performed without running the program, but, to the best of my knowledge, all of them are ultimately some form of applied logic.
• klibertp 11y ago
  It's a guess, but I think GP uses "operational" as a synonym for "imperative". I think I encountered the term "operational semantics" in the context of Prolog programming. Denotational semantics is a term for a kind of semantics which are mathematically pure. IIRC Prolog has both operational and denotational semantics defined and they conflict. There's something about cut operator and tree pruning, but I read this long ago :-)
  • catnaroek 11y ago
    > It's a guess, but I think GP uses "operational" as a synonym for "imperative". Not really. It's also possible to reason non-operationally about imperative programs, e.g., using predicate transformer semantics. It's also possible to reason operationally about non-imperative programs.