home Anil Madhavapeddy, Professor of Planetary Computing  

Using AT Proto for more than just Bluesky posts / Feb 2025

While Bluesky is taking off like a rocket, a number of us moving towards self sovereign digital infrastructure have been looking at how to use the Bluesky network for other uses than just short-form notes. This is possible because of my colleague Martin Kleppmann's hard work on the "AT Protocol" that underpins the Bluesky network. Martin recently gave us a deep-dive into the AT proto in the Cambridge security group, which made me look into other uses of it more closely. As background, you may wish to read his paper on the subject which explains the technical architecture extremely clearly.   […684 words]

# 11th Feb 2025   iconnotes bluesky distributed fediverse ocaml selfhosting

Programming FPGAs using OCaml / Feb 2025

With the vast amount of data we have these days for our planetary computing processing, it's naturally tempting to use more hardware offload. The obvious choice, GPGPUs, are not a great fit for the problem due to the difficulty of unlocking high data parallelism for geospatial data. So it's back to an old technology I worked on twelve years ago in the form of FPGAs!

FPGAs are a very flexible way to execute boolean combinatorial logic, but are notoriously difficult to program. We have two possible angles to explore to address this. One is to design more declarative DSLs for data processing that compile to the FPGAs, such as Michael Dales work on Yirgacheffe or Omar Tanner's work on in-memory compressive computation. The other angle is to work on the low-level API to programming the FPGAs, to get away from Verilog and program in our favourite high-level language...OCaml! KC Sivaramakrishnan and I have started making a list of resources for programming FPGAs in OCaml for our own education.   […1212 words]

# 7th Feb 2025   iconnotes embedded fpga hardware networking ocaml

How to publish custom Homebrew taps for OCaml / Jan 2025

Now that I've switched to a new website, I'm working on open-sourcing its components. I've got a lot of small OCaml scripts that are all work-in-progress, and so not quite suitable to be published to the central opam-repository but I still need be able to run them conveniently on my own self-hosted infrastructure.

I mainly use a variety of macOS and Linux hosts[^1] and I want a workflow as simple as "brew install avsm/ocaml/srcsetter" and have it install a working binary version of my CLI utility. In this case, it's srcsetter, a simple tool I knocked up to generate the responsive images on this website. Luckily, Homebrew has made this really easy for us! They have a BrewTestBot that integrates with GitHub Actions to automate the compilation of binary packages for us, all from a convenient PR-like workflow.   […658 words]

# 31st Jan 2025   iconnotes bushel homebrew ocaml packaging testing til

Foundations of Computer Science / Jan 2025

Here are the various repos used to create the interactive teaching environment we use for 1A Foundations of Computer Science in Cambridge. It may be useful to other professors who are using OCaml in their courses.   […186 words]

# 3rd Jan 2025   iconnotes cambridge compsci computerlab ocaml pembroke teaching

Programming for the Planet / May 2024

I was invited by Mary Sheeran to deliver a keynoted at Lambda Days, and I decided to go along to talk about my work on Programming for the Planet. The conference was a really vibrant crowd and I would definitely go along in future years. It's best summarised via an interview video they took of all the speakers.

# 27th May 2024   icontalks iconvideos biodiversity cloud distributed fp interview ocaml satellite satellites sensing sweden

Towards reproducible URLs with provenance / Jan 2024

This is an idea proposed as a Cambridge Computer Science Part II project, and is available for being worked on. It will be supervised by Patrick Ferris and Anil Madhavapeddy.

Vurls are an attempt to add versioning to URI resolution. For example, what should happen when we request https://doi.org/10.1109/SASOW.2012.14 and how do we track the chain of events that leads to an answer coming back? The prototype vurl library written in OCaml outputs the following:   […323 words]

# 1st Jan 2024   iconideas distributed idea-available idea-medium ocaml provenance web

Parallel traversal effect handlers for OCaml / Jan 2024

This is an idea proposed as a Cambridge Computer Science Part II project, and is currently being worked on by Sky Batchelor. It is supervised by Patrick Ferris and Anil Madhavapeddy.

Most existing uses of effect handlers perform synchronous execution of handled effects. Xie et al proposed a traverse handler for parallelisation of independent effectful computations whose effect handlers are outside the parallel part of the program. The paper [^1] gives a sample implementation as a Haskell library with an associated λp calculus that formalises the parallel handlers.   […162 words]

# 1st Jan 2024   iconideas effects fp idea-medium idea-ongoing multicore ocaml scheduling

Low-latency wayland compositor in OCaml / Jan 2024

This is an idea proposed as a Cambridge Computer Science Part II project, and is currently being worked on by Tom Thorogood. It is supervised by Ryan Gibb and Anil Madhavapeddy.

When building situated displays and hybrid streaming systems, we need fine-grained composition over what to show on the displays. Wayland is a communications protocol for next-generation display servers used in Unix-like systems.[^0]

It has been adopted as the default display server by Linux distributions including Fedora with KDE, and Ubuntu and Debian with GNOME. It aims to replace the venerable X display server with a modern alternative. X leaves logic such as window management to application software, which has allowed the proliferation of different approaches. Wayland, however, centralizes all this logic in the 'compositor', which assumes both display server and window manager roles.[^1]   […267 words]

# 1st Jan 2024   iconideas graphics idea-medium idea-ongoing ocaml

Implementing a higher-order choreographic language / Jan 2024

This is an idea proposed as a Cambridge Computer Science Part II project, and has been completed by Rokas Urbonas. It was supervised by Dmirtij Szamozvancev and Anil Madhavapeddy.

This project aims to implement a functional choreographic language inspired by the Pirouette calculus. This language was meant to make the notoriously difficult process of implementing distributed algorithms easier, while offering a practical execution model for multi-participant programs. Additionally, it aimed to match the expressiveness and performance of similar existing solutions.

The project completed very successfully, and resulted in ChorCaml, an embedded DSL for choreographic programming in OCaml. The language facilitates the implementation of distributed algorithms, while offering a clear syntax and safety via the type system. ChorCaml also improves upon existing alternatives in certain common use cases, both in terms of program conciseness and performance. The practicality of the DSL was verified by successfully implementing well-known distributed algortihms such as Diffie-Hellman key exchange and concurrent Karatsuba fast integer multiplication.   […163 words]

# 1st Jan 2024   iconideas consensus distributed fp idea-done idea-medium ocaml

Gradually debugging type errors / Jan 2024

This is an idea proposed as a Cambridge Computer Science Part II project, and is currently being worked on by Max Carroll. It is supervised by Patrick Ferris and Anil Madhavapeddy.

Reasoning about type errors is very difficult, and requires shifting between static and dynamic types. In OCaml, the type checker asserts ill-typedness but provides little in the way of understanding why the type checker inferred such types. These direct error messages are difficult to understand even for experienced programmers working on larger codebases.

This project will explore how to use gradual types to reason more effectively about such ill-typed programs, by introducing more dynamic types to help some users build an intuition about the problem in their code. The intention is to enable a more exploratory approach to constructing well-typed programs.   […131 words]

# 1st Jan 2024   iconideas functional hazel idea-medium idea-ongoing javascript ocaml types

Effective geospatial code in OCaml / Jan 2024

This is an idea proposed as a Cambridge Computer Science Part II project, and is currently being worked on by George Pool. It is supervised by Michael Dales, Patrick Ferris and Anil Madhavapeddy.

Geospatial data processing is a critical component of many scientific and engineering workflows, from environmental monitoring to urban planning. However, writing geospatial code that scales to multiple cores and makes best use of available memory can be challenging due to the scale of the data involved. To deal with this, we have been developing some domain-specific tools to improve the state of affairs.

Yirgacheffe is a wrapper to the GDAL library that provides high-level Python APIs that take care of figuring out if datasets overlap, and if vector layers need to be rasterised, and manages memory efficiently for large layers. There is only one problem: we would like to write similar code to this, but in a high level functional language rather than an imperative one!   […299 words]

# 1st Jan 2024   iconideas distributed idea-medium idea-ongoing multicore ocaml spatial system

Composable diffing for heterogenous file formats / Jan 2024

This is an idea proposed as a Cambrige Computer Science Part III or MPhil project, and is available for being worked on. It will be supervised by Patrick Ferris and Anil Madhavapeddy.

When dealing with large scale geospatial data, we also have to deal with a variety of file formats, such as CSV, JSON, GeoJSON, or GeoTIFFs, etc. Each of these file formats has its own structure and semantics, and it is often necessary to compare and merge data across different file formats. The conventional solution with source code would be to use a tool such as Git to compare and merge data across different file formats. However, this approach is not always feasible, as it requires the data to be in a text-based format and the data to be structured in a way that can be compared line by line.

This project explores the design of a composable diffing specification that can compare and merge data across heterogenous file formats. The project will involve designing a domain-specific language for specifying the diffing rules, and implementing a prototype tool that can compare and merge data across different file formats. Crucially, the tool should be composable, meaning that it should be possible to combine different diffing rules to compare and merge data across different file formats.   […309 words]

# 1st Jan 2024   iconideas formats idea-available idea-hard ocaml systems

Building bigraphs of the real world / Jan 2024

This is an idea proposed as a Cambridge Computer Science Part II project, and is currently being worked on by Roy Ang. It is supervised by Ryan Gibb and Anil Madhavapeddy.

Bigraphs were originally proposed as a model for the behaviour of ubiquitous systems since interaction between mobile devices is dependent on both placing (locality) and linking (connectivity). However, there has yet to be a bigraph that represents the complete physical world. Such a bigraph will enhance the computer's representation of its location from a simple latitude-longitude pair to a context more familiar to humans: the room it is in, the street the building is on, and the town the street is in. This will allow for location-aware applications and policies about connectivity of mobile devices to work based on the defined locality of buildings, streets and administrative regions.

The physical world has also long been represented by maps. OpenStreetMap (OSM) is a freely-licensed geographic database built by a community of volunteers through the annotation of data collected through surveys, aerial imagery and other free geodata sources. Boasting a user base of 10 million, OSM has labelled buildings, streets and regions with impressive detail comparable with commercial counterparts. The map elements are supplemented with key-value pairs called "tags" that describe characteristics of the element. Tagging conventions vary across countries, but there are standard practices such as the addr tag on buildings to describe its address.   […296 words]

# 1st Jan 2024   iconideas bigraphs distributed idea-medium idea-ongoing networks ocaml spatial

An imperative, pure and effective specification language / Jan 2024

This is an idea proposed as a Cambridge Computer Science Part II project, and is currently being worked on by Max Smith. It is supervised by Patrick Ferris and Anil Madhavapeddy.

Formal specification languages are conventionally rather functional looking, and not hugely amenable to iterative development. In contrast, real world specifications for geospatial algorithms tend to developed with "holes" in the logic which is then filled in by a domain expert as they explore the datasets through small pieces of exploratory code and visualisations.

This project seeks to investigate the design of a specification language that looks and feels like Python, but that supports typed holes and the robust semantic foundations of a typed functional language behind the hood. The langage would have a Python syntax, with the familiar imperative core, but translate it into Hazel code behind the scenes.   […217 words]

# 1st Jan 2024   iconideas functional idea-medium idea-ongoing ocaml specification

State of the OCaml Platform 2023 / Sep 2023

We deliver the annual presentation about the OCaml Platform in the OCaml Workshop at ICFP 2023.

This paper reflects on a decade of progress and developments within the OCaml Platform, from its inception in 2013 with the release of opam 1.0, to today where it stands as a robust toolchain for OCaml developers. We review the last three years in detail, emphasizing the advancements and innovations that have shaped the OCaml development landscape and highlighting key milestones such as the migration to Dune as the primary build system, and the development of a Language Server Protocol (LSP) server for OCaml.

# 1st Sep 2023   iconpapers conference devtools ocaml testing

Displaying the 15 most recent news items out of 114 in total (see all the items).