The Goal:
Raw Bitcoin Script is notoriously difficult to reason about. Writing raw Bitcoin Script today feels like writing Assembly in the 1970s. You have to mentally juggle the stack (`OP_SWAP`, `OP_ROT`), manually manage distinct execution branches, and pray you didn't leave a stack item unconsumed (which crashes the script). My goal was to bridge the gap between complex contract logic and raw opcodes, allowing developers to write readable, compile-time-safe code.
Key Features:
- Imperative Syntax: Write logic using familiar if/else and return statements instead of mental stack juggling.
- Type Safety: First-class support for bool, signature, string, and number types to prevent runtime errors.
- Targeted Compilation: Support for Legacy, SegWit, and Taproot compilation targets.
- Native Primitives: Built-in keywords for timelocks (older, after) and cryptography (sha256, checksig).
You can try it in the browser here (runs via WASM): https://bithoven-lang.github.io/bithoven/ide/
Here is an example of a Hashed Time-Locked Contract (HTLC):
(condition: bool, sig_alice: signature)
(condition: bool, preimage: string, sig_bob: signature)
{
if condition {
// Relative locktime (Sequence)
older 1000;
return checksig (sig_alice, alice_pk);
} else {
// Hashlock verification
verify sha256 sha256 preimage == hash;
return checksig (sig_bob, bob_pk);
}
}
The project is free open source and the academic paper is currently under review. I’d love to hear any feedback. Thanks for checking it out!Even if limited nature, there are many applications of smart contract like hashed-time lock contract, inheritance and multisig contract! You can see examples: https://github.com/ChrisCho-H/bithoven/tree/main/example
I would be glad to anyone who would add example bithoven code!
Quick suggestion - adding simulators for checking all spend paths would add comfort. A lot of comfort. I understand you're doing static analysis on construction, which is great; more safety would be awesome too.
If I missed that you have these, then, I doubly love this! :)
[1] https://bitcoin.sipa.be/miniscript/
[2] https://min.sc/
I understand that Bitcoin Script itself is pretty limited(no mul/div, no bit-operation, no loop), but there must be safe and expressive language as it's standard for UTXO blockchain including bitcoin. The security bug happening because of primitive and hard-to-understand Bitcoin Script could be as severe issue as other advanced programming language bug, as it's directly related to money! Lack of expressiveness also does discourage the possible smart contract application on Bitcoin, which has a high potential value considering mega-economy of Bitcoin.
Bithoven has added expressiveness(and I think it does make a sense for real world impact), and also tried to catch severe agonizing money loss bug with a static anaylzer.