Isn’t the value in being able to verify the design before implementing? It would be more ideal surely to prove correctness of the deployed code, but I still find it very useful.
Fair enough, but to be truly safe you really need the whole pipeline connected. model -> validation -> emitted code.