For all Ledger-like maintainers: a formal semantics

[John Wiegley]

Hi to everyone, and to Simon and Martin in particular:

Something I’ve been working on recently is finding a mathematical formalism
that fully defines the meaning of “double-entry accounting” and thus the math
any Ledger implementation should adhere to if it wishes to implement those
semantics.

Here is the definition I arrived at:

A journal is a term in a free symmetric monoidal category. The principal
object is the free symmetric strict monoidal groupoid 𝕋 over multisets of
accounts: a transaction is a generator whose domain is the multiset of
source accounts and whose codomain is the multiset of destinations; a
journal is then the tensor of its transactions.

Composition is temporal sequencing; the braiding (built by transporting
identities along `add_comm`) says account order never matters. Amounts
appear as a valuation functor into abelian groups, and balance reporting is
the statement that “net flow” is an additive homomorphism out of the free
model. The Pacioli "debits equal credits" invariant is not an axiom; it is
the image of morphisms having equal domain and codomain measure.

Perhaps this sounds like gobbledygook to most, but it defines a very nice,
categorical setting in which to think about accounts, transactions, postings,
amounts, commodities, etc.

These semantics, along with their associated theorems and proofs, have all
been defined and worked out in Lean, using the Lean standard library for the
category theoretical bits.

I (or rather, Claude) then developed a computable representation of these
semantics, also in Lean, that provides a calculational engine for a given set
of transactions. This is now used during Ledger testing to *bisimulate* the
answers produced by C++ Ledger against the answers determined by this
calculational engine. That is: compute the answer both ways and ensure they
agree. This allows me to guarantee that every value computed by C++ Ledger is
indeed a match to the mathematical model.

I’m offering this project as something fully separate from C++ ledger in the
following repository:

https://github.com/ledger/ledger-semantics

If you ask AI to help you with the heavy lifting, it should be trivial to
establish similar bisimulation tests for both hledger and beancount, and in
this way confirm that all of us are indeed “implementing the same idea”. If
not, this either indicates a necessary implementation refinement, or points to
a further abstraction being necessary in the mathematical model. I’m very
interested to know if the latter is the case!

Have fun,
John

[Simon Michael]

Terrific, John. Thanks for sharing !

[Martin Blais]

This sounds riveting, but even armed with the GPT, the level of familliarity and fluidity with the concepts required to grasp its full meaning remains beyond me (I had a quick go at it - I'm getting pieces, but overall no cigar, it's a bit too intensely flavored for a full illumination). So I can't claim to understand well the details of what you wrote--though I do get the spirit of it. It's difficult for me to judge whether it's a tour de force, but it has the contours of it, maybe?

Sorry for the pedestrian questions:

- How realistic is it to compute the verifications on large, realistically sized sets of transactions?
- Have you been able to find bugs in the corresponding C++ code with the verifier?

Thank you,