Finn Hackett

We now have a framework for implementing built-in modules. See `pgo.trans.intermediate.TLABuiltins` for details.

Good to see work's gotten started; commits make sense so far :) Some notes I forgot to add originally: - A non-obvious consequence of these requirements will probably be to...

I'm leaving this on the backburner for now in favour of paper writing, but I wanted to add some context to the original API decision at least. It's intended to...

I think you did probably understand... that was all I was proposing, to have the callsites include `.Read(handle, nil)` and `.Write(handle, nil, someVal)`, rather than `[]tla.TLAValue{}` pasted everywhere. I defer...

Update: - sets of functions (generated using the `[ a -> b ]` syntax) are not iterable, and in fact cannot even be checked for membership if `a` or `b`...

Thanks for the interest + actually trying to build the tool! And, apologies for the slow response. A lot of things just happened (see PR #140 that just merged), which...

Some thoughts, after mulling over the noted challenges. It seems that attempting to work backwards from plain TLA+ invariants, written in terms of the TLA+ output, may be an exercise...

@lemmy thanks for the links. I wasn't aware of these, and they were interesting to check out. Links to material referenced in YT material: - Model-based trace checking: https://arxiv.org/abs/1111.2825 -...

Interesting, thanks for the context. re: capturing internal state, that makes more precise what we might have to deal with, and reinforces the idea that we might have better luck,...

This has already been incorporated into PGo's design by this point.