No, there's no code generation. In that sense, it's more like TLA+.
The code generation is not in the plan, at least, not for the next couple of years until a few prerequisites happen that's not in my control.
The primary reasons for not taking code generation are,
1. It complicates the model spec. My intention is, the spec should be as close to pseudo code as possible that is you ever write pseudo code on your design doc, it should be in fizz.
2. The past experience trying to do complete code generation all failed except for some trivial use cases (like protocol buffers)
--
For the last question, for evaluating expressions, FizzBee uses starlark go library (subset of Python).
Comments
Does this generate executables like Dafny? Or is it more like TLA+ and focused on checking designs?
What’s it using on the backend for checking predicates?
No, there's no code generation. In that sense, it's more like TLA+.
The code generation is not in the plan, at least, not for the next couple of years until a few prerequisites happen that's not in my control.
The primary reasons for not taking code generation are, 1. It complicates the model spec. My intention is, the spec should be as close to pseudo code as possible that is you ever write pseudo code on your design doc, it should be in fizz. 2. The past experience trying to do complete code generation all failed except for some trivial use cases (like protocol buffers)
-- For the last question, for evaluating expressions, FizzBee uses starlark go library (subset of Python).