One behavior, four languages, one BKIR

Method

The operation is a wallet withdrawal over REST: validate the request, check that the wallet exists, that the currency matches and that there are enough funds, debit the ledger, then settle against an external gateway — and if the gateway fails, reverse the debit (a saga). It is idempotent by key. One operation, but dense: predicate and attempt conditions, a pure computation, a transactional effect, compensation, idempotency and a templated error message.

1. A neutral contract. Behavior only — endpoint, JSON shapes, seven acceptance cases and normative rules (decimal money, validation precedence, idempotency). No BKIR vocabulary.
2. Four idiomatic implementations, written independently and following each ecosystem's best practices, each with its own test suite covering the seven cases.
3. Four independent derivations. A BKIR is derived from each implementation's observable behavior, without looking at the others.
4. Comparison. Do they validate, and do they describe the same behavior?

Result: convergence

The four derivations describe the same observable behavior: same flow graph (read → three decisions → compute → transactional debit → settlement with compensation → outcome), same five outputs with the same codes and statuses, same predicate and attempt conditions. They differ only in source (each points to its own implementation) and in wording. Exceptions, Result values and discriminated unions — three different internal mechanisms — collapse to the same named business conditions, as BKIR's guiding principle prescribes: collapse the internal mechanism, expand the observable variation.

Four mechanisms, one condition COND_

How each implementation says “not enough funds”. Java returns a variant of a sealed type, Rust returns an Err, Python raises an exception and TypeScript returns a member of a discriminated union. In BKIR all four are the same thing: a condition named by its business meaning, guarding one output.

var w = wallet.get();
if (w.balance().compareTo(amount) < 0) {
    return new Outcome.Declined(
        money(amount.subtract(w.balance())),
        w.currency());
}

if wallet.balance < req.amount {
    return Err(Failure::Insufficient {
        shortfall: req.amount - wallet.balance,
        currency: wallet.currency,
    });
}

if balance < amount:
    raise InsufficientFunds(
        amount - balance, wallet_currency)

const { balance, currency } = wallet;
if (balance.lt(req.amount)) {
  return { kind: 'declined',
    shortfall: req.amount.minus(balance),
    currency };
}

↓ all four derive to ↓

kind: condition
id: COND_FONDOS_INSUFICIENTES
meaning: "el saldo de la billetera es menor que el monto a retirar"
detection: { kind: predicate, expr: "billetera.balance < amount" }
---
# inside OP_RETIRAR
flow:
  - decision: COND_FONDOS_INSUFICIENTES
    whenTrue: { to: OUT_FONDOS }
outputs:
  OUT_FONDOS:
    result: error
    code: insufficient_funds
    guard: COND_FONDOS_INSUFICIENTES

Four sagas, one edge IO_

After the debit, settlement may fail. Every implementation compensates by hand — a catch, an if let Err, an except — and maps the failure to a 502. BKIR captures it once: an attempt condition (only observable by trying) on the settlement call, and a compensate step on that error edge.

try {
    gateway.liquidar(
        walletId, amount, currency, txId);
} catch (RuntimeException e) {
    ledger.reverse(walletId, amount, txId);
    return new Outcome.GatewayError();
}

if let Err(e) = state.gateway.settle(
    wallet_id, req.amount,
    &req.currency, &tx_id)
{
    state.ledger
        .reverse_debit(wallet_id, req.amount);
    return Err(e.into());
}

try:
    await gateway.liquidar(
        wallet_id, amount, currency, tx_id)
except Exception:
    ledger.credit(wallet_id, amount, tx_id)
    raise GatewayError() from None

try {
  await this.gateway.liquidar(
    walletId, amount, currency, txId);
} catch {
  this.ledger.credit(walletId, amount);
  return { kind: 'gatewayError' };
}

↓ all four derive to ↓

- effect:
    transactional: true
    steps:
      - { bind: transaccionId, use: IO_LIBRO_ASENTAR, args: { walletId: walletId, monto: amount } }
- effect:
    steps:
      - use: IO_PASARELA_LIQUIDAR          # raises COND_PASARELA_CAIDA (attempt)
        args: { walletId: walletId, monto: amount, transaccionId: transaccionId }
        onCondition:
          COND_PASARELA_CAIDA:
            compensate:
              - use: IO_LIBRO_REVERTIR
                args: { walletId: walletId, monto: amount, transaccionId: transaccionId }
            to: OUT_PASARELA                 # 502, net effect zero

See it in the explorer

The four derivations are preloaded in the visual explorer. Open them one after another: the graph is the same; only the source of each Unit points to a different implementation.

Model limits identified

Each derivation records the behavior it could not express declaratively. Most of these limits appear in three or four of the languages, so they belong to the model rather than to a particular language.

• Provenance assumes classes. The source locator has class/method and a single origin; free functions in Rust, module functions in Python and one behavior with four implementations do not fit it well.
• Per-field validation codes. A 422 with a list of {field, code} errors cannot be expressed declaratively from input constraints.
• String normalization in expressions. The expression subset has no upper case/trim, so comparing a normalized currency is lossy.
• Selective idempotency. idempotency cannot say “only successful results are replayed; errors are re-evaluated”.
• Derived output fields. A payload field computed on the way out (the shortfall) has no declarative form.
• Non-deterministic identifiers. A generated UUID has no place to be declared: the environment only admits a clock.
• Implicit precedence. The order of validation checks is expressed only by the order of the flow nodes.