Verifying leftPad() in Whiley

The leftPad(string,int) function simply pads a string up to a given size by inserted spaces at the beginning. For example, leftPad(“hello”,8) produces ” hello”. This little function shot to fame in 2016 when a developer pulled all his modules from NPM, of which one provided the leftPad() functionality. There were two basic issues causing . . . → Read More: Verifying leftPad() in Whiley

Whiley v0.4.2. Released!

And, after a long while, another official release of Whiley is here.  This is something of an interim release whilst other things are brewing in the background.  There also some known issues with this release.  The main changes are:

Fully Qualified Names.  The syntax of fully qualified names has changed.  Specifically, :: is used . . . → Read More: Whiley v0.4.2. Released!

Verifying Bubble Sort in Whiley

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. The algorithm is pretty simple: it loops through an array swapping . . . → Read More: Verifying Bubble Sort in Whiley

Whiley Demo @ Oracle Labs!!

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.

The talk was part of a series of talks I did at various locations across . . . → Read More: Whiley Demo @ Oracle Labs!!

Web IDE gets a Face Lift!

The web IDE for Whiley is the easiest way to run Whiley, and it’s even better after a little face lift!  Here’s the obligatory screenshot:

You can run this on your local machine by cloning the Github repo and running ant run from the command-line.  For now, you can also try it out . . . → Read More: Web IDE gets a Face Lift!

Whiley v0.4.1 released!

The next release of the Whiley Development Kit is upon us.  This is about six months since the last official release and, in the meantime, a lot has been going on!  For example, there have been more than ten releases of the Whiley Compiler (WyC) itself on Maven central.  The main updates are:

RFCs.  . . . → Read More: Whiley v0.4.1 released!

On the Internet and Object-Oriented Programming

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. That is, at least for “classical” object-oriented languages (i.e. not JavaScript).

What . . . → Read More: On the Internet and Object-Oriented Programming

Property Syntax in Whiley

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. I thought it would be interesting to give a quick taste of the syntax.

To understand the purpose of properties, let’s . . . → Read More: Property Syntax in Whiley

On Memory Management and Rust

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). That is, Rust wants safe memory management without garbage collection. This is no easy task, and Rust delivers a . . . → Read More: On Memory Management and Rust

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!  Let’s start with what exactly effective unions are…

Effective Unions

An effective union is a union type which . . . → Read More: Understanding Effective Unions in Whiley