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

This language is designed to bridge the gap between the structured correctness provided by Miniscript and the intuitive control flow syntax similar to C, such as if/else statements and explicit variables. Bithoven aims to offer developers the best of both worlds: the ability to write code that is safe, optimized, and conducive to the rigorous safety requirements necessary for operating within the Bitcoin Script environment, without compromising on the familiar control structures they are accustomed to. By leveraging an LR(1) parser along with static analysis techniques, Bithoven ensures type safety and mitigates common security vulnerabilities, such as unauthorized spending without a signature. The compiler's design is focused on managing stack operations efficiently and optimizing opcodes to support various Bitcoin address formats including legacy, segwit, and taproot.

A significant emphasis in Bithoven's development has been placed on preventing undefined behavior through formally defining the language's semantics and validating its safety through proofs, a process that is thoroughly documented in a paper published on arXiv. An illustrative example provided in the context of an HTLC scenario showcases how Bithoven handles conditional paths with clear, directive syntax, guiding the compiler through explicit stack input definitions and conditional logic to enforce transaction rules like timelocks and signature verifications. The design philosophy of Bithoven emphasizes a clean stack after each operation, mirroring the operational principles of Bitcoin Script while aiming for greater accessibility and expressiveness. Supporting Bithoven’s development and community engagement are resources such as a GitHub repository, a Web IDE, official documentation, and the formal verification paper, which collectively facilitate easy access to Bithoven and invite feedback and collaboration from developers.

The conversation around using a specific compiler as an alternative to Simplicity for implementing STARK proofs and transaction introspection with OP_CAT combined with Schnorr tricks is geared towards evaluating how this compiler could offer a less disruptive method compared to traditional approaches. This exploration stems from a curiosity about the practicality and efficiency of leveraging the compiler's capabilities to achieve desired outcomes in cryptographic operations and smart contract functionalities. The discussion implicitly considers the technical nuances and challenges associated with employing STARK proofs and transaction introspection techniques, which are advanced cryptographic methods aimed at enhancing privacy, security, and scalability in blockchain transactions and smart contracts. By considering alternatives like the mentioned compiler, the discourse highlights ongoing efforts to refine and advance the technological underpinnings of cryptocurrencies and decentralized systems, underscoring the importance of innovation and the development of solutions to address existing limitations and challenges in the field.

Additionally, Bithoven's current version targets strict mainnet safety, disabling experimental opcodes like OP_CAT. However, plans to overload the + operator to compile to OP_ADD for integers and switch to OP_CAT for bytes/strings if OP_CAT becomes enabled on the mainnet have been discussed. This would allow users to verify Merkle paths naturally without manually managing the stack. For Schnorr Introspection, while not yet implemented, the compiler is expected to manage byte concatenation and stack cleanup similarly. This approach indicates a proactive stance toward integrating advanced features in line with user needs and technological advancements, demonstrating Bithoven's potential to serve as a foundational tool for innovative Bitcoin programming practices.