tag:blogger.com,1999:blog-5974817771858035348.post5344598618142544445..comments2019-08-26T03:32:17.583+01:00Comments on Escape Character: Show your workingTom Carverhttp://www.blogger.com/profile/04751782063038275794noreply@blogger.comBlogger3125tag:blogger.com,1999:blog-5974817771858035348.post-32378285605843156472011-05-30T15:04:33.458+01:002011-05-30T15:04:33.458+01:00Certificates are valuable for problems that are ea...Certificates are valuable for problems that are easy to specify. For example, convex optimization software can often give a certificate proving that the computed solution is within some tolerance of the optimal solution. <br /><br />But for many problems, the specification is the hard part. A certification mechanism at best shows that the code satisfies the specification given to the certification authority. But some have argued that most bugs come from <em>missing</em> logic rather than <em>incorrect</em> logic. So if you didn't think to include a case in your code, you may not think to include it in the problem statement given the certifier. More on this idea <a href="http://www.johndcook.com/blog/2010/01/12/software-sins-of-omission/" rel="nofollow">here</a>.Johnhttp://www.johndcook.com/blognoreply@blogger.comtag:blogger.com,1999:blog-5974817771858035348.post-53735679405628239862011-05-30T00:44:42.990+01:002011-05-30T00:44:42.990+01:00Oh, and by the way, isn't most of the forgoing...Oh, and by the way, isn't most of the forgoing a wonderful argument for FP? (Certainly for bills and the like!...)chttps://www.blogger.com/profile/10139341761377884665noreply@blogger.comtag:blogger.com,1999:blog-5974817771858035348.post-6573435613737488332011-05-30T00:41:39.496+01:002011-05-30T00:41:39.496+01:00So, I remember being told a while (=about 1 decade...So, I remember being told a while (=about 1 decade) ago by someone in Formal Methods at UofT that there was a trend towards "certificate-oriented" or "verifiable" programming... Idea being that one aspect of the correctness 'proof' (be it static and absolute or runtime and dynamic) was that your algorithm produced, along with the answer, a "witness" or certificate to the correctness of the answer. The underlying virtue being, of course, that verifying the answer with its certificate might be very much more simple than running (or designing) the algorithm.<br /><br />In an ideal world, one could actually then prove, in the general, that the certificate would always be produced and be valid, and one then had a means of proving the program correct (at least up to whatever abstract model one was considering...)<br /><br />But even in the non-ideal case, it's not a bad way of thinking about correctness in one's algorithm, or even providing user reassurance, or even failsafe checking...<br /><br />-CTWchttps://www.blogger.com/profile/10139341761377884665noreply@blogger.com