Understanding Effective Unions in Whiley

The concept of effective union types in Whiley exposes some interesting features worth considering. In particular, they result in a separation between the readable and writeable view of a type. But, we’re getting ahead of ourselves!

Program Specification in Practice?

Recently, as part of our Programming Languages Reading group, we looked at the paper “Contracts in Practice” by Estler et al., (see here for a copy). This is quite an interesting paper and the authors perform an empirical investigation as to how contracts are used by programmers in practice.

Contractive and Uninhabited Types in Whiley

An interesting feature of Whiley is that it supports true recursive types. These are surprisingly tricky to get right, and recently we came across some interesting examples that the Whiley compiler should (but doesn’t) check for.

Introductory Lecture on Verification in Whiley

We’ve started using Whiley again in my second year course Formal Foundations of Programming. The aim of this course is to introduce students into a range of techniques related to software correctness.

Verification with Data from Untrusted Sources

Recently, I was listening to the latest edition of the Illegal Argument podcast, and it turns out they were discussing Whiley! (about 103:16 minutes in). The discussion was about how verification interacts with data from an untrusted source (e.