Given the spec, formal verification can tell you if your implementation follows the spec. It cannot tell you if the spec if good
Given the spec, formal verification can tell you if your implementation follows the spec. It cannot tell you if the spec if good
I am right now working on an offline api client: https://voiden.md/. I wonder if this can be a feature.
I beg to differ, if a spec is hard to verify, then it's a bad sign.
Of course, you can declare that the world itself is inherently sinful and imperfect, and is not ready for your beautiful theories but seriously.
i see we are both familiar with haskellers (friendly joke!)
That the spec solves the problem is called validation in my domain and treated explicitly with different methods.
We use formal validation to check for invariants, but also "it must return a value xor an error, but never just hang".