I vaguely recall a presentation from Leslie Lamport on TLA+/formal modelling. I might get some details wrong here, but a member of the audience asked 'why not describe a system by examples' (implying it's easier to see some example interactions to start with), and Leslie's reply was it's not rigorous precise enough (not to mention he was visibly angry at the question). I agree it's not precise enough, but for someone starting, an example is good enough rather than choking on rigor. Sure, rigor does matter, but allow me some toehold first!
Just like 'no taxation without representation', there should be 'no formalization without insight'.
Comments
I vaguely recall a presentation from Leslie Lamport on TLA+/formal modelling. I might get some details wrong here, but a member of the audience asked 'why not describe a system by examples' (implying it's easier to see some example interactions to start with), and Leslie's reply was it's not rigorous precise enough (not to mention he was visibly angry at the question). I agree it's not precise enough, but for someone starting, an example is good enough rather than choking on rigor. Sure, rigor does matter, but allow me some toehold first!
Just like 'no taxation without representation', there should be 'no formalization without insight'.