[abreslav]

> * model transforms text into a formal specification

formal specification is no different from code: it will have bugs :)

There's no free lunch here: the informal-to-formal transition (be it words-to-code or words-to-formal-spec) comes through the non-deterministic models, period.

If we want to use the immense power of LLMs, we need to figure out a way to make this transition good enough