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

Bithoven's current design philosophy emphasizes a deliberate choice to forego advanced or general-purpose introspection capabilities in favor of preserving strong static analysis guarantees. This decision clearly positions Bithoven within the landscape of programming tools, highlighting its prioritization of analyzability over expressiveness. As a result of this design choice, certain applications, particularly those resembling covenants, may not be fully supported by Bithoven at this time. The focus remains on ensuring that the platform can offer robust static analysis capabilities, even if it means limiting some aspects of the system's functionality or potential use cases.