Dr. David J. Pearce
Property Syntax in Whiley
Tuesday, March 28th, 2017
Recently, I gave a demo which showed off thew new “Property Syntax” in Whiley. Whilst this is still in the devel branch it will make its way, soon enough, into the next release.
On Memory Management and Rust
Wednesday, February 15th, 2017
Rust is definitely one of the more interesting new programming language I’ve come across recently. Memory management is definitely Rust’s “thing”, and the language wants to have its cake and eat it (so to speak).
Understanding Effective Unions in Whiley
Friday, December 9th, 2016
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!
Mixfix Function Syntax for Whiley
Tuesday, November 15th, 2016
Today I saw an interesting talk about mix-fix function syntax. The idea is to allow a more complex syntax for declaring and calling functions, rather than the very common “uniform” style.
Program Specification in Practice?
Thursday, September 1st, 2016
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.
Flow Typing with Constrained Types
Wednesday, August 3rd, 2016
Flow-sensitive typing (a.k.a. “Flow Typing”) is definitely getting more popular these days. Ceylon, Kotlin, TypeScript, Racket, Whiley all support flow typing in some form. Then, of course, there’s Facebook Flow and the list goes on!
Reference Lifetimes in Whiley
Saturday, May 28th, 2016
The concept of lifetimes was pioneered in the Rust programming language, and builds on earlier notions of regions and ownership types. Lifetimes are considered one of Rust’s “most unique and compelling features”.
Contractive and Uninhabited Types in Whiley
Thursday, April 21st, 2016
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.
Encoding C Strings in Whiley
Thursday, November 12th, 2015
In this post, we’re going to consider representing the classic C string in Whiley. This turns out to be useful as we can then try to verify properties about functions which operate on C strings (e.
Verifying Software with Whiley
Tuesday, October 6th, 2015
A couple of weeks back, I gave a presentation to the Wellington Java User Group. The talk provides a useful introduction to verifying software in Whiley, and shows a bunch of interesting examples.