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.
As announced, I gave a talk last Tuesday at Mama, Zagreb on the role of types in programming as part of the Lamda Zagreb Meetup group. I enjoyed giving the talk and discussing types and programming in general after the talk over a beer. Later on we had a follow-up discussion in the comments section on the event page, which made me happy to see what can be done in Haskell.
On February 6 in Zagreb I’ll be giving a talk on the role of types in programming as part of the Lambda Zagreb group. It will be about pushing the domain into types. I’ll cover various topics, including dependent types and refinement types. An example that I’ll give and that will hopefully be most interesting is about encoding a state machine at the type level. This means that if you try to make an illegal state transition in the code, it won’t compile. My code snippets are going to be in Idris, but I’ll provide Haskell and Scala equivalents where applicable.
The talk is going to be in Croatian, but I’ll do my best to have the slide deck ready in English just in case.
What is a common problem in programming is to use types that are too generic for a particular problem. If a too generic type is used, it leads to allowing values in types that don’t make any sense for the particular problem at hand, which leads to unforeseeable errors at runtime. For example, you might want to say that a particular number has to be greater than 5, i.e., x > 5. This kind of constraint is nice to have because it supports a pattern where illegal values are not representable. That way you avoid throwing exceptions at runtime when you get a value that doesn’t meet needed constraints, which allows for referential transparency, which allows for functional programming, which in turn allows for easier reasoning about your programs. In general, type systems in programming languages don’t have a way of representing a constraint like x > 5.
The type system in Scala is based, among other things, on subtyping polymorphism, which is also known as inheritance in the object-oriented community’s parlance. Wikipedia defines it as:
Subtyping (also called subtype polymorphism or inclusion polymorphism): when a name denotes instances of many different classes related by some common superclass.
Many programmers and developers see it as a great concept that helps with organizing source code. However, there are also serious downsides to it.
Scala is a programming language that heavily relies on the JVM platform. While there are many reasons to consider this to be an advantage for Scala, it also comes with many downsides given the language design choices. One big problem with Scala is equality, i.e., checking if values are equal.
The third week of my Google Summer of Code 2016 project is behind me and I started changing KLEE‘s source code in order to meet the goal of the project. The goal is to get KLEE plugged into Debian’s Debile, and for that to happen KLEE has to support Firehose, an interchange format for results for (static) analysis tools.
If you are interested in how to use Scala as a scripting language and how that works behind the scenes, there’s a nice blog post about it.
As of last week I’ve finally gave the Scala programming language a try, as in I’ve actually started coding in Scala. I don’t want this to be a yet-another way of writing plain old imperative, hence next to incomprehensible and unmaintainable code. Therefore, lately I’ve been putting a lot of energy into thinking how to program functionally. You can say I’m finally delivering on my earlier promise to code in Scala. In other words, seeing lots of bad/imperative code during an internship can do you good, i.e. it can make you want to program in a better way. Continue reading