# Programming using logic assistants

What does a mathematician do?
They play with theorems.

What does a smart mathematician do?
Knows the theorems, but not necessarily remembers and knows all of them on top of their head. In fact, that’s probably impossible. They use proof assistants or logic programming languages.

I think a similar conclusion can be drawn for programmers.

At my current job, I get to work with different parts of a complex system constantly. I cannot and it is not expected from me to remember all the parts or decisions for the system, so often we need input from either Architecture or Product Managers. This is where communication jumps. We use JIRA/HipChat and other tools to ease our communication.

But I was thinking, what if we could use logic programming languages as our personal assistants to draw conclusions about decisions of the system’s behaviour?

Consider a complex system S, together with parts P = {P_1, P_2, …, P_N}. Consider all possible inputs as I = {I_1, I_2, …, I_N}.
Each part might need different inputs. So we can state that f : P -> I.
Consider we’re working on part P_K. So f(P_K) is the set of inputs needed for that part specifically, i.e. f(P_K) is a subset of I.

All of the values in f(P_K) are unknown. But at some point in time, you get to know their values. And at this point is where you bring a decision.

We can take Prolog as an example. We start with an initial knowledge base, which probably explains some of the values of f(P_K), and as we get more and more input, we keep improving the knowledge until the point f(P_K) = , i.e. no further input is required to bring a decision.

This is good because you get to re-use the knowledge base in the future, and also every time f(P_K) gets an update you can bring the conclusions based on that without going through recalling all the details, which saves a lot of time.

Most of the tasks are tiny and “easy” to go and evaluate the logic for through your mind, but once you get a lot of tasks you can’t remember every tiny detail about each one of them. This is what computers are for. 🙂