David J. Pearce (Blog)

Verifying Bubble Sort in Whiley

Tuesday, December 19th, 2017

Bubble sort is a classic sorting algorithm with lots of well-known issues. It’s been a long time since I thought much about this algorithm. But, it turns out to be an interesting verification example for Whiley, as it has some interesting loop invariants.

Whiley Demo @ Oracle Labs!!

Thursday, August 24th, 2017

Recently, I gave a demo of Whiley at Oracle Labs in Brisbane which they have kindly put up on YouTube: The actual demo itself starts around 11:30s, so you might want to skip on to that.

On the Internet and Object-Oriented Programming

Wednesday, June 21st, 2017

The rise of the internet over the last, say, two decades has been pretty unstoppable (we all know that). But, is it now affecting the prominence of object-oriented programming? I’m going to try and argue in this post that: yes, it is.

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”.

1
2
3
4
5