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

11–20 of 72 posts

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

#11

Post by drewcoo »

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 results, dude, component C is messed up" combined with

"component C never promised that behavior and if you look at our spec it even says so!"

That's an example of your "does not match what was expected" case.

I think most of formal methods is an academic waste of time. Whether they take a more formal or a more practical approach, I see high value in contract tests and data flow analysis because they're more likely to catch the bugs that cross Conway's code/org boundaries.

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

#12

Post by nh23423fefe »

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 (λ (…

> if we

Who is this we? The people who understand mashed with the ignorant who put in no work?

> to democratise

So that those in the know can be further diluted with dabblers who contribute nothing and complain about their ignorance?

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

#13

Post by miloignis »

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…

You don't need to prove everything against a complete spec, you can prove that things have particular properties you care about, from higher level behaviors like user data can only be accessed by the user down to there are no out of bounds array accesses.

You could prove some complex data-structure to be a correct implementation of some logical data-structure and then prove that your service won't deadlock.

There are a ton of interesting, impactful properties to prove that aren't "create a complete specification and prove the implementation refines it", and even that usage I think is more impactful for removing bugs and vulnerabilities than you're giving it credit for - even something as simple as sorting, Java had a bug in their Timsort implementation for a decade which was discovered when trying to verify it with formal methods: http://envisage-project.eu/wp-content/uploads/2015/02/sortin... ). Note too that if you compiled the simplest/easiest-to-understand spec for something like sorting you'd get something like bubble sort, not Timsort, though you are much more likely to want the latter.

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

#14

Post by Taikonerd »

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.

I've had the same thought. Formally proven code can give powerful security assurances (cf. Project Everest[1]), but it's also very, very labor-intensive. I've heard rules of thumb like, "100x as much time to prove the software correct as to write it in the first place."

If LLM systems are going to give us a virtual army of programmers, I think formally proving more systems software (device drivers, browser engines, etc.) would be a great use of their time.

[1]: https://www.microsoft.com/en-us/research/blog/project-everes...

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

#15

Post by flir »

nh23423fefe wrote: post #12
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 (λ (…

> if we Who is this we? The people who understand mashed with the ignorant who put in no work? > to democratise So that those in the know can be further diluted with dabblers who contribute nothing and complain about their ignorance?

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

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

#16

Post by im_down_w_otp »

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…

This kind of, “Just what the heck in this pile of parts is impacting the other stuff and how is the other stuff impacting this part?” was precisely the angle we took with our V&V tools.

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

#17

Post by miloignis »

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 (λ (…

That snippet is the result of printing out the internal structure of the proof, not how the proof was actually written. You'll notice that what a human actually wrote and would normally read is the code block mentioned directly above in TFA, which is much more sensible:

  lemma nat.add_comm : ∀ n m : ℕ, n + m = m + n
  | n 0     := eq.symm (nat.zero_add n)
  | n (m+1) :=
    suffices succ (n + m) = succ (m + n), from
      eq.symm (succ_add m n) ▸ this,
    congr_arg succ (add_comm n m)
Also, this example proof is explicitly about math (the commutativity of addition on natural numbers), so it's appropriate and not surprising that it uses mathematical notation.

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

#19

Post by jgeada »

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…

Yes, this!

What would be helpful is if formal methods were powerful enough to be able to prove contracts and assertions about expectations and invariants; however, all formal systems I've experienced are not powerful enough to do this at scale in any interesting program, not without spending way more time reconstructing the entire system in the formal world, with the attendant likelihood of introducing spec bugs in that reconstruction.

It is entirely different in the world of hardware, where the specification in many cases is the RTL and the thing being proved is the, supposedly identical, physical implementation.

Post reply on HN