Some AL pseudocode: the when construct

Protocol Design
1

/!\: This is all highly speculative pseudocode.

Suppose my intent is to unconditionally transfer my space buck S to Bob. This is simple enough to write:

S.transfer(Bob)

This is imperative-looking, and deals with a “space buck” object. What it compiles to is the intent-carrying logic which requires

  • the presence of S in the consumed set,
  • the presence of an equivalent S' owned by Bob in the created set
    and carries
  • the authorizations necessary for transfer of a space buck
    Meanwhile, the space buck’s logic tests things like
  • “transfer” is a valid space buck operation,
  • the right authorization is present to perform this operation.

Getting more complicated, consider

when let E = EarthBuck(owner: me) {
  S.transfer(E.owner())
}

This won’t grow a sensible syntax until we’re clear on more things (in particular, it binds a counterfactual object in this example; have to treat these as though they’re concrete objects); the important thing here is the semantics of “when”.

In imperative code, we can use constructs like “if”: this performs a test, and then picks a code path to follow based on the result of this test.

“when” is different. “when” is a sort of “anthropic if”; its condition is always true! It feels like an “if” to use, but if the condition were false, we never would have executed to begin with. It compiles to conditions which fail resource logic validity, causing no state changes to happen.

But it feels like an “if” to use. The ergonomics are forwards, which is the important part. And it compiles to an “if” in backwards-land. It’s just that a backwards “if” run backwards isn’t an “if”, it’s a “when”.

2 Likes