Is it common practice to transform requirement specifications into predicate logic for functional programming?

Question

I've recently been assigned to work on a small project which is being implemented in Haskell. Coming from an OO/imperative background, I'm used to converting requirements/user-stories into use-cases and sequence diagram prior to coding.

However, the Haskell project that I have been assigned to, the team prefers to transform the user requirements into predicate logic proposition/statements. I was aware of logic being used in safety critical systems and formal methods for software engineering, but not so much in day to day programming. Is this common practice in the FP realm? Where can I learn more about this?

It seems like a natural way to 'model' the requirements and derive the 'functions' from the predicates along with writing down the necessary type specifications for the functions to operate on. But is that how it is done/recommended in practice or is it something peculiar to my team?

(I've tried searching extensively prior to asking this question here. Searching for "requirements specification in functional programming" (and different keyword synonyms and combinations) doesn't lead to anything meaningful.)

Answer 1

I will say that it's not limited to functional programming, it's more related to the goal of the project. By using predicate logic (higher order logic) you can create prove for the logic used in the requirement. Translating the logic into functional languages is probably easier. It's also possible to then translate the proven functional language implementation into procedural languages to get some kind of proven way of implementing it.

If we can prove the program then we don't need to test it. Even if a program passed 1000 tests, it's still not proven. Obviously, it's not easy to create the proofs so we just create tests instead.

You might also want to search for theorem prover, isabelle/hol.

Answer 2

That's one way to deal with functional programming. It tends to fall out from the flowcharts and data flow diagrams of the "old days." Instead of thinking in terms of objects, functional programming tends to focus on what actions need to be performed. The data becomes incidental, bits of fluff to carry along to hold on to what you're trying to do.