You Got Your Idris in My C++! A First Look at Denotational Design

*
Accepted Session
Short Form
Intermediate
Scheduled: Thursday, June 25, 2015 from 10:00 – 10:45am in B304

Excerpt

Programmers gripe that we have two kinds of programming languages: the ones we write in for fun, and the ones we write in because we have to. We may enjoy coding that weekend project in Agda, but we have to leave that smile behind on Monday morning when we go back to Java or C++.

But is that really the case? Or can we find a way of bringing the expressiveness, the rigor, or the fun of our favorite languages into our day jobs?

Description

Denotational Design is a practice espoused by Conal Elliott, David Sankel, and others. The gist is that you model your problem in a language that supports the way you think, then translate that model into your implementation (which may be in a different language).

Elliott’s approach is a full-on plunge into the deep, mathematical waters of type systems. We’re just going to dip our toes into the pool today. We’ll start with a few C++ APIs that went wrong. We’ll back up into a simpler notation, clean up our models, and then re-implement them more simply.

By the end of the talk, you’ll have a few basic ideas on how to connect your “thinking” languages to your “doing” languages. The next steps are to try these techniques on your own, and to spice them up with more formal mathematical models.

Tags

C++, Idris, api

Speaking experience

I've spoken several times, including at OSCON, Open Source Bridge, PNSQC, and Cascadia Ruby Conf.

Speaker