From logic and math to code. For dummies. Part I: Basics

We are used thinking, that software development is a kind of exact science. At least we believe in it. How otherwise are we going to prove our customers that our soft will work? But in reality, things usually are not so clear.

So what’s wrong with software development?

The goal of programming at the end is to move business requirements from the proposal on natural language to concrete processor commands that will make a machine do what we really wanted. The problem is that informal logic and natural language are very hardly adapted to formal systems, if even possible completely. Apparently, because evolutionary our mind and consciousness were built on other laws.

But somehow we do this migration and sometimes even more or less properly. It gives food for thought, that one day we can do this migration automatically.

No need in developers anymore! Yay!

Such thoughts excite many futurists and journalists. Recently Microsoft even created a neural network which can write code by itself using more informal instructions from humans.

Formal and informal logic

But fundamentally, the relationship between informal and formal logic are not clear yet, complete processing of natural language is not solved yet and don’t forget, that requirements in informal logic can easily have errors which can not be imperceptible.

So let’s image the situation from freelance board:
Premise: Bob is a programmer
Premise: Programmer develops software
Premise: Facebook is software
Conclusion: Bob can develop Facebook

If you as a freelancer would ask the customer to explain what “Facebook” means, in order to write the implementation mostly correctly, he or she should design a formal logic system describing entity “Facebook”.

Ideally, such description should look like the greatest attempts of humanity to build logically proved definitions: Euclid’s “Elements” or Spinoza’s “Ethics” where the final definitions (geometry and ethics) are inferred from atomic notions like point, line, circle, god, nature and consciousness.

Also, all statements should be proved correctly, be valid, complete and consistent with other known theorems. And even then you can get in trouble, for example, because of Gödel’s incompleteness theorem, which says that even in the formal complete system you can come across with unprovable statements (e.g Liar Paradox).
Probably customer would then think that you got crazy and will find someone else for making just some kind of social network.

So we are not going to consider perspectives of developers replacement with neural networks, instead of that, step by step, we’ll consider the magic of transition from formal logic to code. So let’s go.

Formal logic

The first one who introduced the notion of formal logic (or analytics how it was called those time) and described it’s basics was a great guy — Aristotle. He discovered 3 of 4 laws of logic (here and further I’ll use C++ logical operators, which every developer is familiar with, instead of math ones):

  • Law of identity (A == A)
  • Law of noncontradiction (A && !A == false)
  • Law of excluded middle (!A || A == true)

Don’t remind anything?

Right! Boolean algebra, which treats values only as truth values and extends formal logic rules.
The fourth rule was discovered by another great logic guy — Leibniz and called “Principle of sufficient reason”. By the way, he introduced 1 and 0 as true and false respectively. 
This rule is not formalized so well as Aristotle’s rules but has to be used making any type of judgments. Other words, we must firstly somehow prove, that our true/false values are really so, to be able to make any conclusions.

But what can we do in real life with such low-level logic? Basically nothing. We need some rules to build more abstract proposals. 
And here Propositional calculus comes! This guy allows us to analyze logical structure of really complicated proposals, which we deal with in real life.

The hardcore part is coming soon.

To be continued