Re:Formal methods only solve half my problems
by aeneasmackenzie on Friday June 03, 2022 @08:59PM
(#31615731)
Leslie Lamport had an essay about this. Without a spec, even if it's just "Serves the user's homepage", your program is not even wrong.
Re:Formal methods only solve half my problems
by xupybd on Friday June 03, 2022 @10:59PM
(#31616529)
Thanks! I'll have a read. Your comment helps clarify the situation.
Re:Formal methods only solve half my problems
by rramadass on Friday June 03, 2022 @11:32PM
(#31616703)
You may find https://markusvoelter.medium.com/the-evolution-of-decision-t... helpful. He also has a lot on DSLs which is worth reading.
There is also a more powerful version of Decision Tables called Tabular Expressions (from D.L.Parnas) which you can use.
A nice succinct reference to Formal Methods is Concise Guide to Formal Methods by Gerard O'Regan.
I think simplified versions of Formal Methods can be used profitably for your use-cases. Start with Assertions, Design-by-Contract and Decision Tables.
That being said, FM is an enormous spectrum; if you squint a little, writing really good user stories could be considered a 'formal specification'. There's a really good paper from Amazon about model checking (Newcombe 2014 IIRC) where they make the bold statement that "Doing the math didn't help us find that many mistakes, nor did using the model checker; the thing that was most helpful was sitting down and forcing ourselves to come up with really good definitions. Like what does X really mean?" So it doesn't have to be as complicated as you think.
So if you want to start as simple as possible, I would recommend something like this: https://www.hillelwayne.com/post/decision-table-patterns/