The IT field has been aware for decades that software can kill people and so we are witness of this fact again with Boeing and its two airplanes 737 Max crashing and killing everyone on board due to erroneous software in the accompanying MCAS system. Continue reading
If your program can have only two legal states, what sense does it make to extend a Boolean type with a third data constructor to account for the possibility of an “illegal program state”? Use a coproduct type with a Boolean type on the right instead. Make illegal program states irrepresentable in your types. I’m baffled by folks that insist on having their three-valued Boolean type.
The upcoming Tuesday I will be giving a talk at the IEEE Croatian Section on function totality. The talk will take place at the University of Zagreb, the Faculty of Electrical Engineering and Computing.
Edsger Dijkstra said the following of abstraction:
“The purpose of abstraction is not to be vague, but to create a new semantic level in which one can be absolutely precise.”
Abstraction is a cornerstone of programming a complex software system. Without it, a complex software system is a complicated software system. In this article I will explore an important tool in achieving abstraction in programming: function totality.
Software has become ubiquitous. It’s all around us and in us. It is in our pockets, in cars, airplanes, stock exchanges, our bodies, our offices and in lots of other places. As a computer scientist and a programmer I’ve worked in aeronautics, computer security, finance and automotive industry and I can say that software engineering is a mess. The Atlantic demonstrates this point rather thoroughly in an interesting piece on the state of the software engineering profession. I agree with the article and here I will briefly tie this to what I see to be a solution, split into four parts: 1) the licensing of professional software engineers, 2) a requisite degree in computer science, 3) mandatory formal methods in software development, and 4) all software should be free as in freedom.
Software testing has been an important, if not prevalent way of checking software correctness. In this article I will tell how have my doctoral dissertation on testing and verification of imperative software as well as my work experience after the studies led me to typed functional programming, which consequently gave me a different perspective on automatic software testing. Furthermore, I’ll explain why functional programming and static type systems are important for software correctness.
Philip Wadler makes a fun note about today’s programming languages: “Most of you use programming languages that are invented, and you can tell, can’t you?” I recommend watching his whole talk Propositions as Types!
For fast searching of source code that avoids peeking at your build files use the ag tool from Debian’s silversearcher-ag package, like this: ag -s –haskell “what” where.
You might think it’s only imperative programmers that don’t see value in function totality, but neither do many functional programmers. The ability to abstract in programming is severely impaired when totality is ignored. A programmer should strive to work in a programming language with a compiler that supports totality checking, such as Agda and Idris.
Momentarily, the Haskell IDE Engine (HIE) is in a bad shape. In its version 0.2.2, it eats a huge amount of memory, much more than my machine can provide (I have 8 GB in total). Users have already reported this, and even though there is a memory leak in GHC, Haskell IDE Engine developers haven’t started tackling this problem yet. What you can do in the meantime is to provide runtime system (RTS) options to an engine executable to limit its heap and stack memory sizes. For example, you can write a wrapper script around the
hie executable that would run it with the following RTS options:
hie +RTS -c -M1500M -K1G -A16M -RTS --lsp $@
This limits the heap size to 1500 MB and the stack size to 1 GB. The executable will crash once it surpasses these limits, but your editor (e.g., Atom) should restart it. In other words, HIE will keep on crashing and restarting in a loop, which is ugly, but that’s what we have now.