the interface between specification and proof is not so clear, as one often has to look at the proof to understand the spec. And if we see something weird in the proof, that’s a good indication that something is off.
Yeah this is like if I say something is green how do you know that my green is your green? The proof of the mathematically modeled system is in no shape attached to the symbols that implement it unless its the same program or youre doing trace refinement. And then theres no way of proving that the program is correct in serving the business function unless you run it out. Quite computationally irreducible, the state machine of building state machines
whattheheckheck · · focus · HN ↗
Yeah this is like if I say something is green how do you know that my green is your green? The proof of the mathematically modeled system is in no shape attached to the symbols that implement it unless its the same program or youre doing trace refinement. And then theres no way of proving that the program is correct in serving the business function unless you run it out. Quite computationally irreducible, the state machine of building state machines