An imperative, pure and effective specification language
This is an idea proposed in 2024 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.
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
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
Links
ideasRelated News
- Planetary Computing / Jan 2022
- Retrofitting effect handlers onto OCaml / Jun 2021