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

21–30 of 72 posts

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

#21

Post by AlotOfReading »

Taikonerd wrote: post #14
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, e…

I've had extremely poor results attempting to get current LLMs to generate proofs, for code or otherwise.

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

#22

Post by voxl »

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

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

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

#23

Post by rsrsrs86 »

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…

Formal methods have their applications and specific use cases. It all depends on how much is at stake, economically.

I suggest checking into Alloy, which is far easier to work with. It feels like writing a SQL schema, but you get bounded model checking and much more.

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

#24

Post by ogogmad »

AlotOfReading wrote: post #21
Taikonerd wrote: post #14

Earlier quoted context omitted.

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, e…

I've had extremely poor results attempting to get current LLMs to generate proofs, for code or otherwise.

Combining it with AutoGPT (or the ideas it's based on) and a formal prover like Lean might be the answer. Have you tried?

Basically, if you don't allow GPT to iteratively write, execute, criticise and then correct its code, you won't get good results.

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

#25

Post by ta1748 »

rsrsrs86 wrote: post #20
jderick wrote: post #18

We use formal at Apple to verify hardware. We are always looking for good people in this area.

Do you have more to share? I use Alloy at work and research and would love to learn about how Apple uses FM.

This is the easiest way to get an idea for what is happening and what experience is needed:

https://jobs.apple.com/en-us/search?search=formal&sort=relev...

There are several different niches, and HW formal is likely using different tools and methods than SW formal, though there is overlap. Anyways there is room for a wide range of experience/skills/background in a variety of different areas.

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

#26

Post by UncleEntity »

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?

Yep, like the olden days where the only people “in the know” knew Latin. Or, before that, Greek.

Then someone had to come along and invent the printing press.

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

#27

Post by Joker_vD »

UncleEntity wrote: post #26
nh23423fefe wrote: post #12

Earlier quoted context omitted.

> 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?

Yep, like the olden days where the only people “in the know” knew Latin. Or, before that, Greek. Then someone had to come along and invent the printing press.

> Or, before that, Greek.

Greek (or koine, for that matter) was pretty much street vernacular in the Roman/Byzantine empire during that period you're likely talking about.

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

#29

Post by jderick »

rsrsrs86 wrote: post #20
jderick wrote: post #18

We use formal at Apple to verify hardware. We are always looking for good people in this area.

Do you have more to share? I use Alloy at work and research and would love to learn about how Apple uses FM.

Apple is pretty tight lipped about revealing the details of our work. Formal is a bit of a niche area, but you can find some info online.

Here is a course taught at UT with some slides from guest lecturers from industry that looks like a decent overview:

https://www.cerc.utexas.edu/~jaa/verification/

Also, the main conference in the area is FMCAD, you can find a lot of related work there. More recently the conference has moved more towards software, but if you look at some of the older proceedings you can find a lot of hardware related stuff.

https://www.fmcad.org/

There is decent amount of overlap between formal for hardware and software, so if you study one you will likely have enough background to get started in the other.

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

#30

Post by sirwhinesalot »

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…

Forall (n: Nat)

Is perfectly reasonable.

If conciseness was that important theorem provers would have syntax like APL.

Post reply on HN