Show HN: Bithoven – A high-level, imperative language for Bitcoin Smart Contract

8 comments

·December 15, 2025

Hey HN! I’m a researcher working on Bitcoin smart contracts, and today I’m releasing Bithoven—a high-level imperative language that compiles to native Bitcoin Script (Legacy, SegWit, and Taproot).

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!

Visit

OsrsNeedsf2P

Looks pretty neat. As someone who hasn't followed Bitcoin for the last 5 years, what are some things people have built with smart contracts? Also, are Bitcoin smart contracts Turing Complete and suffer the same gas issue as ETH where you don't know how much gas you need?

hyunhum

Bitcoin Script is non-turing-complete in nature(so no gas issue!), so does Bithoven. Bithoven doesn't extend Bitcoin Script Opcodes(which requires consensus upgrade on the protocol), but inherit and abstract for the expressiveness. Moreover, it supports static analysis to cache some known security bugs.

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!

vessenes

I love this! Thanks for making it.

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! :)

hyunhum

Yes, simulator definitely would! Actually I'm planning to add input constructor or simulator to generate safe symbolic/static inputs for users, and simulate with symbolic script engine to validate even stricter. As it might require the Bitcoin Script interpreter (with symbolic execution for things like signature), I left it as a near future work.

hyunhum

I omitted one detail in the original post: Bithoven uses an LALR parser generator (Lalrpop) to strictly define the formal grammar and avoid ambiguities when parsing to the AST!

hyunhum

Docs: https://bithoven-lang.github.io/bithoven/docs/

wslh

I don't think it makes any sense except for fun, Bitcoin scripts are pretty limited and there are a lot of previous work [1][2][3][4][5].

[1] https://bitcoin.sipa.be/miniscript/

[2] https://min.sc/

[3] https://docs.scrypt.io/

[4] https://github.com/sapio-lang/sapio

[5] https://github.com/ivy-lang/ivy-bitcoin

hyunhum

I've researched the previous works surely, and actually contributed miniscript(the most notable one in industry AFAIK) quite a lot(https://github.com/rust-bitcoin/rust-miniscript). Contributions to the previous work has actually motivated me to research and implement this. As you may know, miniscript, while could be safer as restricted policy lang, is not really expressive enough to express many bitcoin opcodes(e.g. + and - op), and really hard to understand and write for dev not familiar with Bitcoin Script.

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.