> I think TLA+ is a great fit for what you want to do.
I'm very happy to hear that.
> What problems are you facing?
Generally, the problem of formally specifying a program in set theory and first-order logic syntax before choosing implementation details, such as the language to program it in.
I have to give more thought to how I would describing specific problems. I've started with a program I want to write that I've already modelled informally. I'll edit this post later to explain it.
I'm very happy to hear that.
> What problems are you facing?
Generally, the problem of formally specifying a program in set theory and first-order logic syntax before choosing implementation details, such as the language to program it in.
I have to give more thought to how I would describing specific problems. I've started with a program I want to write that I've already modelled informally. I'll edit this post later to explain it.