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

31–40 of 72 posts

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

#31

Post by commandlinefan »

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 in the work", even outside of software (like fitness and music) - but in over 30 years of software development practice, I've never met anybody who was applying formal methods at all, much less to achieve defect-free software. If it could deliver what it promised even with a "mere" five years of dedicated study, I'd expect it to be more widespread by now.

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

#32

Post by ratmice »

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

One thing which perhaps is not captured well in the article, is that rather unlike when reading/writing source code, where stepping through lines of code is a relatively uncommon task only done debugging. For interactive theorem provers it is a given. He discusses the bottom up & top-down approach to the solving goals with tactics & otherwise, but typically in both cases you will be stepping through expressions to get a better understanding. They generally aren't written to be read from just the source text alone.

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

#33

Post by markusde »

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!

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

#34

Post by mcguire »

cgio wrote: post #7
whatever1 wrote: post #6

I like there is us who like formal methods and guarantees of correctness for our code. And then there are the others who now generate approximately code with large language models that mostly runs. They are winning.

It’s a repeat of search & hope/trust (Google) vs define and query (semantic web) and yes they are winning and will win. Fine tuning your scope for extreme accuracy might be less efficient a strategy than fine tuning your loader for extreme speed

In most situations, a half-assed answer quickly will a beat a good answer slowly.

Most.

""Software should be reliable.""

Reliability is not usually worth the effort. Most software is not used enough, or not important enough, to make any effort worthwhile. In almost all systems, errors are created at every step and propagate through the system routinely without causing problems.

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

#35

Post by tsimionescu »

sirwhinesalot wrote: post #30
tsimionescu wrote: post #8

Earlier quoted context omitted.

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.

Why is forall any less formal than ∀? Or Nat less formal than ℕ? Especially when these are symbols that most will have learned in high school?

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

#36

Post by prisonguard »

flir wrote: post #15
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?

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

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

#37

Post by prisonguard »

voxl wrote: post #22
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

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

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

#38

Post by guai888 »

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 has value in safety related software. When you are developing software for airplane, rail, automobile and nuclear power station, any tools that might improve safety merit consideration.

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

#39

Post by rqtwteye »

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.

I think it probably needs to be a specialized combination of LLM and hardcoded knowledge.

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

#40

Post by mcguire »

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 far as I know, but is very good for demonstrating value correctness (RTE automatically generates assertions for numeric runtime errors, for example) and many memory errors.

If you are familiar with Ada, check out SPARK (https://www.adacore.com/about-spark), which is similar to Frama-C but has a much better interface in the AdaCore GNAT toolkit and IDE.

Both work similarly: Assertions in normal Ada or C code as well as the code itself are translated into SMT statements and fed to a SMT solver to find counterexamples---errors.

I have some blog posts from several years ago about Frama-C:https://maniagnosis.crsr.net/tags/applied%20formal%20logic.h... (And I really should get back into it; it's a lot of fun.)

If you are not familiar with Ada or C, Dafny (https://dafny.org/) is another option based on .NET and devoleped at Microsoft. It seems nigh-on perfect for this approach. (The language uses a garbage collector.) At the time I was looking, there was little documentation on Dafny, but that seems to have improved.

Post reply on HN