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

The development of Bithoven v0.0.1 is specifically focused on ensuring mainnet safety with strict adherence to SegWit/Taproot protocols, hence, currently excluding the use of experimental opcodes like OP_CAT. This decision underscores a commitment to reliability and security in the blockchain's operation, prioritizing established safety measures over the incorporation of untested functionalities.

In an innovative approach to handling Merkle paths, there's an ongoing plan to make the syntax more intuitive for users. By redefining the + operator, it will perform double duty: executing as OP_ADD when dealing with integers and switching to OP_CAT for operations involving bytes or strings, assuming OP_CAT becomes enabled on the mainnet. This dual functionality aims to simplify the verification of Merkle paths by allowing natural expressions like sha256(a + b), thus eliminating the need for manual stack management.

Regarding Schnorr Introspection, although not yet implemented, there is an openness to exploring this feature through similar means. By leveraging the compiler to manage byte concatenation and stack cleanup, the goal is to streamline the integration of such advanced features. The request for raw script snippets utilizing introspection logic from peers indicates a collaborative approach to refining this aspect, suggesting that real-world use cases could significantly influence the compiler's experimental branch development.