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.