Extending Isabelle/HOL's Code Generator with support for the Go programming language

TL;DR

This paper extends Isabelle/HOL's code generator to support Go, enabling extraction of functional programs into an imperative language with features emulated through Go constructs.

Contribution

It introduces a novel approach to generate Go code from Isabelle/HOL, handling imperative features and integrating as an add-on library.

Findings

Go code generation successfully integrated into Isabelle/HOL.

Emulation of data types, pattern matching, and type classes in Go.

The extension allows practical extraction of verified programs into Go.

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.