Typed Functional Programming and Software Correctness

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.

Continue reading

Gave a Talk on Types in Programming

Courtesy of Ivica Dimjašević

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.

Continue reading

Announcing: Talk on the Role of Types in Programming

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.

Refinement Types

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.

Continue reading

A Subtyping Polymorphism Misfortune

Courtesy of Jin

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.

Continue reading

Firehosing KLEE

Courtesy of Kelly

Courtesy of Kelly

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.

Continue reading

I’m Into Scala

ScalaAs 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