Re:The Case for Formal Verification (2013)
by a-saleh on Monday April 21, 2014 @05:25AM
(#7620376)
As a q/a by profession, I allways wonder, how to have some better assurances that the software I have does what it is supposed to.
I believe I have even incidentaly reimplemented quick-check on several occasions.
When we were working in Clojure for a little while, I wondered if it might be possible to combine contracts and logic programming, to verify that contracts don't contradict each other on compile ... and then I realized, that for more complex constraints I might need to solve halting problem.
On the other hand, I remember how much productivity I gained, after I wrapped our json library in simple macro, that verified that the data I feed it conforms to schema (that was before prismatics schema existed, or even core.typed).
I believe I have even incidentaly reimplemented quick-check on several occasions.
When we were working in Clojure for a little while, I wondered if it might be possible to combine contracts and logic programming, to verify that contracts don't contradict each other on compile ... and then I realized, that for more complex constraints I might need to solve halting problem.
On the other hand, I remember how much productivity I gained, after I wrapped our json library in simple macro, that verified that the data I feed it conforms to schema (that was before prismatics schema existed, or even core.typed).