Extending Isabelle/HOL's Code Generator with support for the Go programming language
Terru Stübinger, Lars Hupel
TL;DR
This work extends Isabelle/HOL's Code Generator by adding Go as a target language, addressing the challenge that Go is not a functional language. It accomplishes this by translating Thingol programs into a restricted, imperative Go fragment using shallow embeddings, with data types simulated via a per-constructor struct set and a universal interface to emulate sums; type classes are encoded through a dictionary mechanism. The implementation is provided as an AFP entry (Go-AFP) and demonstrated through case studies, including a re-port of an existing formalisation from Scala to Go, showing compatibility and practical usability. The approach preserves the existing Code Generator pipeline, enabling Go code to be produced without rewriting Isabelle formalisations, while outlining limitations and opportunities for deeper Go integration and library use in future work.
Abstract
The Isabelle proof assistant includes a small functional language, which allows users to write and reason about programs. So far, these programs could be extracted into a number of functional languages: Standard ML, OCaml, Scala, and Haskell. This work adds support for Go as a fifth target language for the Code Generator. Unlike the previous targets, Go is not a functional language and encourages code in an imperative style, thus many of the features of Isabelle's language (particularly data types, pattern matching, and type classes) have to be emulated using imperative language constructs in Go. The developed Code Generation is provided as an add-on library that can be simply imported into existing theories.