axiom

In development (for fun)

axiom will be a proof-producing compiler-optimiser that operates on a small purpose-build expression only language. Using axiom in a command-line interaction may look like this:

$ axiom optimise "(x + 0) * 1"
Source:         (x + 0) * 1
Result:         x
Source cost:    5
Result cost:    1
Proof:          result.proof
Status:         Verified improvement

The axiom checker then can run seperately:

$ axiom-check \
    --source="(x + 0) * 1" \
    --result="x" \
    --proof=result.proof
ACCEPTED

axiom language

The axiom language being optimised may consist of:

• Variables
• Constants
• Addition
• Subtraction
• Multiplication
• Bitwise operations
• Shifts
• Comparisons
• Conditional expressions