4 ms·
> that doesn't seem an unreasonable assumption to make in this case Not that I don't agree with you but I find it a common failure mode of HDs to just never re
by __alexs 12y ago
> that doesn't seem an unreasonable assumption to make in this case
Not that I don't agree with you but I find it a common failure mode of HDs to just never reply to things. I guess it's also a common failure mode of network systems too.
Can Coq detect that you are enforcing I/O timeouts in a way that guarantees finite time?
- pja 12y agoI don't know whether this particular proof models IO timeouts - might have a poke at it and see what it's doing if I have time later. More generally, Coq is "just" a well integrated proof tool & I can't see any reason why you couldn't include such features but at some point you have to draw the line and be explicit about what it is that you're actually proving: if your proof assumes data store responsiveness then it's OK for it to do that so long as you're explicit about the resulting limitations IMO. The goal of ever increasing model fidelity is a rabbit hole from which the programmer/prover might never return otherwise :)
- clarus 12y agoYes, for now we assume that there is exactly one answer for each external call to the system: https://github.com/clarus/coq-chick-blog/blob/master/Spec.v#l21 https://github.com/clarus/coq-chick-blog/blob/master/Spec.v#... In practice, we should use a timeout in the implementation of all the external calls, but we did not and our model to not enforce it.