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.
Another direction to investigate is also translating the same code into OCaml 5, and use the new effect system to handle IO and mutability in the source language code. This would allow for multiple interpretations of the program to execute depending on the context:
- an interative JavaScript-compiled (or wasm-compiled) tracing version that records variable updates
- a high performance version that batches and checkpoints variable updates and deploys parallel execution
1 Background Reading
- Toward a Live, Rich, Composable, and Collaborative Planetary Compute Engine, PROPL 2024.
- Patrick Ferris's first year PhD report (available on request to students interested in this idea).
- Retrofitting effect handlers onto OCaml
2 Links
3 Outcome
Max Smith completed this as a Part II project, with a slightly different focus in the end as we changed our minds after starting the project. He worked on building Uio, a query language for pulling values out of structured data files. The code is on GitHub, which is private for now (ask him if you would like a look).
For example, reading two fields out of every JSON file in a zip archive normally looks like this with general purpose libraries:
Zip.open_in "data.zip" @@ fun zip_handle ->
let files = Zip.entries zip_handle in
List.iter (fun file ->
let decompressed = Filename.temp_file "" ".json" in
Zip.copy_entry_to_file zip_handle file decompressed;
let json = Yojson.Basic.from_file decompressed in
let version = json |> member "version" |> to_int in
let name = json |> member "name" |> to_string in
printf "name %s, version %d" name version
) files
The same thing in Uio:
let open Uio.Infix in
Eio_main.run @@ fun env ->
let iterator = Uio.load ~env "data.zip/*/[name, version]" in
Uio.iter_fn iterator (string @$ int) @@ fun name version ->
printf "name %s, version %d" name version
From his dissertation:
Not only does the Uio query language improve readability, it also improves efficiency. General purpose libraries like Yojson do not know in advance what values the user is interested in, so they read and parse the entire file just in case. In a scientific context, these files can be huge. Since the Uio query is available in advance, the parser can stop reading the file as soon as the "version" and "name" keys have been processed. Memory usage reduces from O(n) to O(1) [..]
Most importantly, Uio is designed to be easily extensible – modules can be injected at run-time that seamlessly slot in, to add support for unusual file formats with minimal set-up. This means that a uniform syntax can still be used even for these novel or rarer file formats. A Universal Data Access DSL, Maximilian Smith, May 2026