Comment by hintymad
5 years ago
Not sure if prolog or formal methods are good examples here, as they are pretty hard programming language. Yes, they can be used to specify a system, but they also require human ingenuity, aka strong intelligence, to get right. Prolog may be easy for some people, but I did spend inordinate amount of time to understand how to use cut properly, and how to avoid infinite loops caused by ill-specified conditions in my mutually recursive definitions.
As for formal methods, oh, where shall I even begin? The amount of time to turn something intuitive into correct predicate logic can be prohibitive to most of professionals. HN used to feature Eric Hehner's Practical Theory of Programming. I actually read through his book. I could well spend hours specifying a searching condition even though I could solve the search problem in a few minutes. And have you checked out the model checking patterns (http://people.cs.ksu.edu/~dwyer/spec-patterns.ORIGINAL)? I honestly don't know how a mere mortal like me could spend my best days figuring how to correctly specify something as simple as an event will eventually have between an event Q and an event P. Just for fun, the CTL specification is as follows:
``` G(Q -> !E[!R U (!P & !R & EX(P & E[!R U (!P & !R & EX(P & E[!R U (!P & !R & EX(P & !R & EF(R)))]))]))]) ```
As I said, formally specifying a system, no matter what tools one uses, is essential complexity.
I want to see formal methods used more in lieu of writing standards documents. If you go read a standards document, say for 5G wireless, you'll find it's largely formal specification awkwardly stated in English and ad hoc diagrams. It would be better to just write out something formal (with textual annotations as a fallback) and have a way to translate that to readable language.