A brainf*ck dialect in Lean, written in terms of DNA bases.

The language uses DNA base letters to encode Brainf*ck commands. All other characters are ignored, and # starts a line comment.

Accessine accesses data points:

• >: A Increment the data pointer (to point to the next cell to the right).
• <: a Decrement the data pointer (to point to the next cell to the left).

Crementine increments or decrements the pointed data:

• +: C Increment (increase by one) the byte at the data pointer.
• -: c Decrement (decrease by one) the byte at the data pointer.

Grabanine grabs data from pointer to output, or from input to pointer:

• .: G Output the byte at the data pointer.
• ,: g Accept one byte of input, storing its value in the byte at the data pointer.

Targetine targets the next data pointer based on conditions:

• [: T If the byte at the data pointer is zero, then instead of moving the instruction pointer forward to the next command, jump it forward to the command after the matching ] command.
• ]: t If the byte at the data pointer is nonzero, then instead of moving the instruction pointer forward to the next command, jump it back to the command after the matching [ command.

The interpreter is implemented as a purely functional, total program in Lean 4:

• Tape: Zipper-style infinite tape (List Nat, Nat, List Nat)
• Jump table: Precomputed T/t loop matching for O(1) jumps
• Execution: Fuel-based loop (defaults to 1M steps) ensuring totality
• No mutation, no IO in semantics — all effects are explicit in the state

You need Lean 4 (v4.27.0) installed via elan.

# clone the repository
git clone https://github.com/erhant/dnalang.git
cd dnalang

# build the project
lake build

Write a .dna file using the instruction set above, then run it:

lake exe dnalang <file.dna> [-n] [input bytes...]
# -n: print the result bytes as numbers instead of strings

For example, the included Hello World program:

# CCCCCCCCTACCCCTACCACCCACCCACaaaactACACAcAACTatactAAGA
# cccGCCCCCCCGGCCCGAAGacGaGCCCGccccccGccccccccGAACGACCG
lake exe dnalang examples/hello.dna
# => Hello World!

MIT