Physics, Proof and Aquaculture...What do they have in common?
Since the 19th century with the work of Fourier, physicists have used dimensional analysis to check the correctness of their mathematical reasoning. The basic idea is that you can only add like with like, so you can add a quantity of kilograms to another quantity of kilograms (or grams) to get a total of a new quantity of kilograms. However, it does not make sense to add a quantity of meters cubed (volume) with a quantity of kilograms (mass)!
Here is an example of dimensional analysis: if you multiply density by volume, you get mass.
Dimensional analysis has become an essential foundational utility in physics and is routinely taught in physics courses to students around the world because it eliminates a whole host of errors in reasoning.
In software engineering, a similar phenomenon has taken hold with the use of type systems. Like dimensional analysis in physics, type systems are used in the design of some programming languages to ensure that only compatible entities are combined with each other, usually by checking the compatibility of parameters and arguments to functions or procedures. Not all languages incorporate such checking, and programs written in languages which lack type systems are therefore much more likely to encounter unexpected problems, such as ‘bugs’ or security issues.
At PanLogica, we use programming languages with type systems throughout our work, but we asked ourselves: could we take these ideas further in our software engineering practice? After all, we have a strong mathematical heritage, and both dimensional analysis in physics and type systems in programming are means of checking the correctness of reasoning, so in essence, they are a form of mathematical proof of correctness.
Doing this benefits our customers by automating the checking of the correctness of our software beyond testing automation, by proving that it is impossible for our software to go wrong wherever such methods can be applied.
To go beyond conventional applications of type systems, we needed an automated deduction system capable of constructing proofs about new properties of our software. Fortunately, the type system of the language we use is Turing-complete, which means that it is a programming language in its own right. This has enabled the team here at PanLogica to incorporate newly automated proof checking directly into our programming practice.
And the result? We are seeing our work pass testing the first time, it feels like magic! We are delivering the most correct, robust and capable software ever seen in the aquaculture industry, thanks to a little help from the power of mathematical proof.
PanLogica has been empowering aquaculture producers around the globe, including the largest and most innovative, for more than ten years. We invite you to contact us for a more detailed explanation of Neptune and PanLogica and how it can help your business optimise the timing of investments.