Re:A taste of Coq and correct code by construction
by mrkeen on Monday September 04, 2023 @05:13AM
(#37378624)
> I'm not sure if mathematical proof is the way to go. There's just too much code to cover for this approach to be realistic.
It may be unrealistic, but people are doing it anyway. It may be the case that there are just a few Leslie Lamports capable of doing this stuff, and it's unrealistic to expect the rest of us to.
But even if that's the case, I still want them to publish their code as libraries, so I can reach for tools that will work - even if I couldn't have proved it myself.
And if this whole mathematical/proofy way of doing things is a dead end (which I strongly disagree with - we're just at the beginning!) then it's no big deal, because we are already really good at turning JSON into stack traces.
It may be unrealistic, but people are doing it anyway. It may be the case that there are just a few Leslie Lamports capable of doing this stuff, and it's unrealistic to expect the rest of us to.
But even if that's the case, I still want them to publish their code as libraries, so I can reach for tools that will work - even if I couldn't have proved it myself.
And if this whole mathematical/proofy way of doing things is a dead end (which I strongly disagree with - we're just at the beginning!) then it's no big deal, because we are already really good at turning JSON into stack traces.