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 as part of my Planetary Computing project.
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: