Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

What I've Learned About Formal Methods in Half a Year

jakob.space

Post reply on HN
Print view View original

41–50 of 72 posts

Re: What I've Learned About Formal Methods in Half a Year

#41

Post by rqtwteye »

markusde wrote: post #33
rqtwteye wrote: post #2

I wonder if AI systems like ChatGPT will be helpful in this area. Something that’s able to track all requirements of a system and understands the code enough to validate it against the requirements.

Yeah, I'm cautiously excited about how AI and FM might work together. I don't think LLM's can ever be trusted to verify programs itself, but anything which can reduce the annotation overhead for programmers is a super useful thing!

I don't think a pure LLM approach will work (or maybe it will, who knows?). I am more thinking of a hybrid that combines LLM or other AI with some hardcoded knowledge for this domain

Re: What I've Learned About Formal Methods in Half a Year

#42

Post by nodogoto »

prisonguard wrote: post #37
voxl wrote: post #22

Earlier quoted context omitted.

Something else important to note: this proof of commutativity of addition on natural numbers is definitely _not_ how you normally write these proofs in Lean. Here is a closer approximation to how someone would actually write the proof in Lean: lemma add_comm (a b : ℕ) : a + b = b + a := begin induction a with a IH, rw (add_zero b), rw (zero_add b), trivial, rw (add_succ b a), rw (succ_add a b), rw IH, trivial end

thank you for explaining, but do i need a special keyboard just to type out the natural number type?

No, you just type \N. You can also use `nat` instead if you prefer.

Re: What I've Learned About Formal Methods in Half a Year

#43

Post by prisonguard »

tsimionescu wrote: post #8
prisonguard wrote: post #4

I've always thought theorem proving to be about proving equality of the function and the result. Lean to me is not only obscure but unapproachable by someone from a non-mathematical background. Take this snippet for instance theorem nat.add_comm : ∀ (n m : ℕ), n + m = m + n := λ (n m : ℕ), nat.brec_on m (λ (m : ℕ) (_F : nat.below (λ (m : ℕ), ∀ (n : ℕ), n + m = m + n) m) (n : ℕ), nat.cases_on m (λ (_F : nat.below (λ (…

I don't think you have any chance of approaching formal methods if the notation is a stumbling block. The difficulty and verbosity of formal proofs is huge even with the very concise mathematical notation. And learning the notation itself is a very small stumbling block compared to learning the actual theorems and logic that you need to use. So while I am not a fan of mathematical notation for general programming (wh…

there has to be a better way for a beginner to learn Lean even with the faintest high school mathematics recollection.

I can still do theorem proving in Idris excluding the mathematical notation and still learn concepts such as totality, covering, equality etc

Re: What I've Learned About Formal Methods in Half a Year

#44

Post by mcguire »

jgeada wrote: post #5

If I had complete enough specifications for any interesting program that formal methods would be interesting, I think I would just be easier to hit compile on that spec. Yes, there are a subset of interesting bugs related to edge cases, but the real problematic bugs are when what the software does does not match what was expected, even if nobody really could articulate what was expected in the first place. The art of…

One advantage of formal methods is in determining "what was expected" (including all the goofy edge cases) without having to burrow into the details of code.

Take a look at Alloy (http://alloytools.org/) and TLA+ (https://lamport.azurewebsites.net/tla/tla.html) for example. (Or even the ancient Z ("Zed") notation (https://www.cs.cmu.edu/~15819/zedbook.pdf)).

Re: What I've Learned About Formal Methods in Half a Year

#45

Post by cscurmudgeon »

commandlinefan wrote: post #31
jgeada wrote: post #5

If I had complete enough specifications for any interesting program that formal methods would be interesting, I think I would just be easier to hit compile on that spec. Yes, there are a subset of interesting bugs related to edge cases, but the real problematic bugs are when what the software does does not match what was expected, even if nobody really could articulate what was expected in the first place. The art of…

> I think I would just be easier to hit compile on that spec I have a hard time not being similarly skeptical about formal methods. They promise the ultimate holy grail of software development - release software with zero defects - but demand what appears to be years of study before you actually see results. On the one hand, there's lots of examples of techniques and tactics that promise amazing results if you "put i…

I have met tons of folks who have used this in practice. It tends more applied in domains where errors can be costly. E.g., this won't be that much useful in the JS/NodeJS.

https://www.amazon.science/publications/how-amazon-web-servi...

https://link.springer.com/chapter/10.1007/978-3-642-34281-3_...

> They promise the ultimate holy grail of software development - release software with zero defects

Thats a straw man. It is just another tool.

Re: What I've Learned About Formal Methods in Half a Year

#46

Post by mcguire »

drewcoo wrote: post #11
jgeada wrote: post #5

If I had complete enough specifications for any interesting program that formal methods would be interesting, I think I would just be easier to hit compile on that spec. Yes, there are a subset of interesting bugs related to edge cases, but the real problematic bugs are when what the software does does not match what was expected, even if nobody really could articulate what was expected in the first place. The art of…

I think the interesting part isn't in a single component's edge cases at all, but in how complex webs of many, many things interact. I've yet to see a hard debugging problem that didn't boil down to something like, in the best of possible worlds: "component A expected something to meet promise FOO when it calls component B, because that's obvious, right?" combined with "component B just passes requests and routes res…

That's actually what many formal tools excel at. Of course, you have to do have to define "never promised that behavior" which is extra work that nobody wants to do.

Re: What I've Learned About Formal Methods in Half a Year

#47

Post by noisenotsignal »

commandlinefan wrote: post #31
jgeada wrote: post #5

If I had complete enough specifications for any interesting program that formal methods would be interesting, I think I would just be easier to hit compile on that spec. Yes, there are a subset of interesting bugs related to edge cases, but the real problematic bugs are when what the software does does not match what was expected, even if nobody really could articulate what was expected in the first place. The art of…

> I think I would just be easier to hit compile on that spec I have a hard time not being similarly skeptical about formal methods. They promise the ultimate holy grail of software development - release software with zero defects - but demand what appears to be years of study before you actually see results. On the one hand, there's lots of examples of techniques and tactics that promise amazing results if you "put i…

Years of study are definitely not required to get up and running! I attended a 3 day workshop for TLA+ and spent ~2 weeks modeling a new project that my team was working on. I found lots of potential edge cases that would result in data inconsistencies without even having to write tests or think about how to articulate the issue in the first place, as the model checker is able to output the exact program flow that results in the error.

You still need to make sure your implementation matches the spec, but that’s an easier task than squashing concurrency bugs, let alone figuring out how to repro in the first place! The hope is that by writing the spec you avoid a good chunk of errors from the start instead of encountering them one by one.

Re: What I've Learned About Formal Methods in Half a Year

#48

Post by mcguire »

prisonguard wrote: post #4

I've always thought theorem proving to be about proving equality of the function and the result. Lean to me is not only obscure but unapproachable by someone from a non-mathematical background. Take this snippet for instance theorem nat.add_comm : ∀ (n m : ℕ), n + m = m + n := λ (n m : ℕ), nat.brec_on m (λ (m : ℕ) (_F : nat.below (λ (m : ℕ), ∀ (n : ℕ), n + m = m + n) m) (n : ℕ), nat.cases_on m (λ (_F : nat.below (λ (…

Brute force string search:

    /*@
      // There is a partial match of the needle at location loc in the
      // haystack, of length len.
      predicate partial_match_at(char *needle, char *haystack, int loc, int len) =
        \forall int i; 0  needle[i] == haystack[loc + i];
     */

    /*@
      // There is a complete match of the needle at location loc in the
      // haystack.
      predicate match_at(char *needle, int n, char *haystack, int h, int loc) =
        \valid(needle + (0 .. n-1)) && 0 = 0 ==> match_at(needle, n, haystack, h, \result);
     behavior failure:
        ensures \result == -1 ==>
          \forall int i; 0 
            !match_at(needle, n, haystack, h, i);
     */
    int
    brute_force (char *needle, int n, char *haystack, int h)
    {
      int i, j;
    
      /*@
        loop assigns i, j;
        loop invariant 0 
          !match_at(needle, n, haystack, h, k);
       */
      for (i = 0; i = n) {
          return i;
        }
      }
      return -1;
    }

Re: What I've Learned About Formal Methods in Half a Year

#49

Post by tsarfox »

mcguire wrote: post #40

I'm not sure if the author is here, or if my comment attempt was successful. So, can I suggest you take a look at a third leg of the formal methods stool? If you are familiar with C, check out Frama-C ( https://frama-c.com/ ) and the WP and RTE plugins. The approach is based on Tony Hoare and EWD's axiomatic semantics ( https://en.wikipedia.org/wiki/Hoare_logic ). It does not have a good memory management story, as f…

Sorry to hear you had issues with my comment system. Comments are invisible until I manually approve them, but I'm not seeing anything new in the database right now. Did you get any sort of error code? The system should let you know if e.g., the answer to the captcha was wrong.

I do mention SPARK at the end of the article. I'm not familiar with Frama-C so I'll check that and your blog posts out. Thanks for sharing!

Re: What I've Learned About Formal Methods in Half a Year

#50

Post by nh23423fefe »

prisonguard wrote: post #36
flir wrote: post #15

Earlier quoted context omitted.

raises hand I'd like more tools that involve me putting in no work, please. They help me achieve my real-world goal faster.

making thing obscure and less obvious is anti-intellectual, its getting harder and harder for new developers to gain a footing in software development also why tools like chatGPT have gained so much popularity

3 assertions with no implications
Post reply on HN