alt Hacker NewsBut the code produced from the formal spec would still be nondeterministic. And I believe CodeSpeak doesn't wish to regenerate the entire program with each spec change, but apply code changes based on the changes to the spec. Maybe there could be other benefits to formalisation in this case, but determinism isn't one of them.
Replies
vidarh • yesterday at 5:56 PM
It doesn't matter if the code is different if the spec is formal enough to validate the software against it.
I have no idea about codespeak - I was responding to the comments above, not about codespeak.
➕ show 1 reply
Even with classic compilation, it is only the semantic behavior that is preserved.
What the Church–Rosser property/confluence is in term rewriting in lambda calculus is a possible lens.
To have a formally verified spec, one has to use some decidable fragment of FO.
If you try to replace code generation with rewriting things can get complicated fast.[2]
Rust uses affine types as an example and people try to add petri-nets[0] but in general petri-net reachability is Ackerman-complete [1]
It is just the trade off of using a context free like system like an LLM with natural language.
HoTT and how dependent types tend to break isomorphic ≃ equal Is another possible lens.
[0] https://arxiv.org/abs/2212.02754v3
[1] https://arxiv.org/abs/2212.02754v3
[2] https://arxiv.org/abs/2407.20822