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

KLEE: It Ain’t Gonna Do Much Without Libraries

Library. Courtesy of Viva Vivanista.

Library. Courtesy of Viva Vivanista.

KLEE comes with a nice tutorial. The tutorial demonstrates how to use KLEE on a few examples. All but one of the examples operates on self-contained or so-called closed programs. These example programs do not use any external functionality, including essential things such as a library for printing out to the standard output. However, if a program is to communicate with other programs or to do more complex computation, it is very likely it will need to rely on external functionality. Enter libraries.

Continue reading

Working on Imperative Programming Code Ain’t Fun

Have you ever read someone else’s code that has more than 20 lines? If so, I’m sure you came to appreciate a few things about software engineering. For example, the code being documented comes in very handy. Another crucial thing is: in what ways and if at all does this and this method/function change the state of its input parameter and possibly a hidden state somewhere at lower layers?

Courtesy of Mark Skipper

Courtesy of Mark Skipper

Continue reading

Going with JVM Languages


export lang_path=scala:java:aspectj:clojure:${lang_path}

IBM punched card Accounting Machines

IBM punched card Accounting Machines in 1936

When choosing a programming language to write in, one of the most important concerns is the trade off between the writing abstraction level and computational resources needed to execute the program you’re writing. If we look back to the beginning of the 20th century, we will see that machines were programmed by inserting wire jumpers into removable control panels. Since those days, the program writing abstraction level has been rising. Today we don’t write applications by fiddling with wires, punch cards, or do anything that involves moving physical components around. When programming, we write software that most of the time completely abstracts away the hardware the software will be running on. (Exemptions to this are operating systems, firmware, and other software that has direct access to the underlying hardware.) Applications we write don’t interact with the hardware directly. Instead, there are a few layers of abstractions that take care of concerns such as the type of display device, which processor is running program instructions, etc. Continue reading