KHoon: A Formal Semantics of Hoon in the K Framework

Abstract

Hoon, a programming language with several unusual properties, which is intended for use as a smart contract language, currently lacks a formal semantics, and this poses challenges in terms of verification. This project aims to overcome this issue by providing a formal semantics for Hoon using the K framework. The resulting specification covers approximately a quarter of the language’s features and is accompanied by a test suite consisting of 131 tests to validate the specified features. Furthermore, this paper presents various claims about the Hoon specification that can be proven using the theorem prover in the K framework. Nonetheless, further work is needed to complete the specification and enable its potential future applications.