<div dir="ltr"><div class="gmail_default" style="font-size:small"><br></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Feb 23, 2017 at 10:33 AM, Patrick Chkoreff <span dir="ltr"><<a href="mailto:patrick@rayservers.net" target="_blank">patrick@rayservers.net</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">Perry E. Metzger wrote on 02/22/2017 10:07 AM:<br>
<br>
>> In addition to empirical testing, I often think in terms of pre- and<br>
>> post-conditions and loop invariants, which in conjunction with<br>
>> correctness-preserving code transformations, are in effect a<br>
>> quasi-formal proof.<br>
><br>
> One popular technique in formal verification is the use of Hoare logic<br>
> and its descendants, which is where the notion of pre and<br>
> postconditions comes from.<br>
<br>
</span>Yes, I learned the technique by reading Tony Hoare back in the 80s.<br></blockquote><div><br></div><div><div class="gmail_default" style="font-size:small">​Prof Hoare was my college tutor.​</div><br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Basically what I've done is, instead of maintaining a *separate* entity<br>
called a "proof", I have aimed to make my code itself an ongoing sort of<br>
proof.  By that I mean whenever I transform the code, I do it in a<br>
systematic way which, if applied correctly, is guaranteed either to (1)<br>
maintain the original correct behavior of the code, or (2) alter the<br>
behavior of the code in a way which is also correct.<br></blockquote><div><br></div><div><div class="gmail_default" style="font-size:small">​Most of it can be automated, the main issue is providing invariants for loops and arriving at the specification in the first place. Getting a specification correct is as hard as getting a program correct.</div><div class="gmail_default" style="font-size:small"><br></div><div class="gmail_default" style="font-size:small">The biggest value I think there is to formal methods is actually in forcing people to design systems that are simple enough to be tractable. I have removed about 10,000 lines of code from the Mesh code over the past year by refining the design.</div><div class="gmail_default" style="font-size:small"><br></div><div class="gmail_default" style="font-size:small">The tools I use do allow me to code at a very high level, which is very close to a specification language. My goal is to take the language in which I specify the problem as close as I can to the structure of the problem domain. </div><div class="gmail_default" style="font-size:small">​</div><br></div><div> </div></div></div></div>