Bithoven: A Formally Verified, Imperative Smart Contract Language for Bitcoin

The introduction of Bithoven, a new smart contract language, aims to bridge the gap between the structured correctness that Miniscript offers and the familiar imperative control flow syntax similar to C, such as if/else statements and explicit variables. This endeavor seeks to combine ease of use for developers with the rigorous safety requirements necessary for operating within the Bitcoin Script environment. The primary goal is to allow developers to write code that is both safe and optimized, without sacrificing the intuitive control structures they are accustomed to.

Bithoven leverages an LR(1) parser along with static analysis techniques to ensure type safety and mitigate common security vulnerabilities, such as unauthorized spending without a signature. The compiler is designed to manage stack operations efficiently (e.g., OP_SWAP) and optimize opcodes (e.g., transforming OP_EQUAL + OP_VERIFY into OP_EQUALVERIFY), while also providing support for various Bitcoin address formats including legacy, segwit, and taproot. A significant emphasis has been placed on preventing undefined behavior by formally defining the language's semantics and validating its safety through proofs, a process thoroughly documented in a paper published on arXiv.

An illustrative example provided, an HTLC scenario, showcases Bithoven's handling of conditional paths with clear, directive syntax. This demonstrates how the language can guide the compiler through explicit stack input definitions and conditional logic to enforce transaction rules, such as timelocks and signature verifications. The design philosophy of Bithoven emphasizes a clean stack after each operation, achieved by starting statements with commands like verify, which ensures no residual values remain on the stack. This approach mirrors the operational principles of Bitcoin Script while aiming to be more accessible and expressive.

Resources supporting Bithoven’s development and its community engagement include a GitHub repository, a Web IDE, official documentation, and the aforementioned formal verification paper. These tools not only facilitate easy access to Bithoven but also invite feedback and collaboration from developers interested in exploring this innovative smart contract language. This open invitation for community feedback underscores the project's commitment to refinement and adaptability, acknowledging the importance of addressing potential edge cases and enhancing the language’s robustness in future releases.