7 ms·

Can someone ELI5 this, please?

• aaronsnoswell 2y ago
  [flagged]
  • thechao 2y ago
    That's a shockingly good Socratic dialog that maps fairly well! I've not read your dialog in detail; nor have I read this blog article enough times to know if the mapping is correct. However, a quick glance shows that it's in the same ballpark!
  • dev-jayson 2y ago
    This is probably the longest comment I've ever seen on this platform.
  • aaronsnoswell 2y ago
    Downvotes - explain why?
    • ajb 2y ago
      Because if they wanted an LLM answer they could paste it into an LLM themselves.
      • CamperBob2 2y ago
        It's not an answer, it's a dialogue. One that's literate and erudite enough to be interesting. Hackers aren't supposed to be knee-jerk reactionaries. Do better... or at least, vote better.
        • theamk 2y ago
          That is an answer in form of dialogue. There is no point in engaging with LLM-generated comments, as person posting them is not an original author, you cannot ask them for clarification, discuss minor point, or point to inaccuracy. That's why LLMs are best left to personal, interactive context, and attempts to paste LLM replies into comments should be downvoted.
          • 73kl4453dz 2y ago
            Also, ivanbakel's answer was good ; the llm one was long and unfocused.
• ivanbakel 2y ago
  The traditional Hoare logic is the "partial correctness" form - if the program state satisfies a precondition, and executing the program terminates with some other state, then the second state satisfies the postcondition. This is "correctness" in the sense it overapproximates all executions: if the postcondition says something about the state being "good", the precondition ensures you end in a "good" state, but perhaps there are more "good" states than actually reachable ones. It's partial because nothing is said about non-terminating executions. A more recent idea was to flip this correctness logic to get an incorrectness logic, which says if you can reach a "bad" state (this is useful for bug detection.) In such a logic, you only want to know about reachable states, so the formula gets flipped: if the final program state satisfies the postcondition, then there must be a program state satisfying the precondition that can execute the program and terminate in that final state. The difference between these two logics is one axis of this cube. There are other possible logics: you can ask if a precondition is necessary - that is, is the postcondition only reachable from states satisfying the precondition? It turns out there are two orthogonal approaches to stating such a property, and they form the other two axes of the cube.