Business requirements still have a measure of ambiguity and "do what I mean" to them. They are more formal than natural language, sure, but fall far short of the formalism of a declarative programming language. This is a big part of the business partnership underlying most Agile methodologies. If the formal spec could be handed off, then it would be and Waterfall would work better in enterprise settings. Instead, the team is constantly requiring feedback on the requirements.

So I guess I still see declarative languages as being part of the tech stack and something tantamount to AI being needed to handle all the "do what I mean" that accompanies business process documentation.

I think honestly the problem is a lack of tech literacy. I've seen spec sheets that are glorified database and json schemas in a spreadsheet, put together by BAs and translated by hand.

It could be done directly if every BA had enough programming knowledge to put together schemas and run CLI tools to verify them.

> had enough programming knowledge to put together schemas and run CLI tools to verify them.

That's quite a lot of programming knowledge. It makes some sense to decouple the business-oriented from the more technical roles - BA's trying their hand at coding is how you get mammoth Excel spreadsheets and other big-balls-of-mud.

I'd prefer not to.

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.