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

Formal methods and the future of programming

blog.janestreet.com

Post reply on HN
Print view View original

121–129 of 129 posts

Re: Formal methods and the future of programming

#121

Post by jdw64 »

rramadass wrote: post #120
jdw64 wrote: post #119

Earlier quoted context omitted.

Thank you for your comment. I may have been a bit rude, but that was not my intention. I trust you will understand. Anyway, there are points in your thinking that I also resonate with. I realize now that some of my arguments were too rough. I am not going to withdraw the point that formal specifications cannot always be specified with perfect accuracy, but I do think there were some shallow aspects to what I said. I…

That's all right; no need to feel bad. These things happen when communicating in forums like this. Btw - Another useful way to think about model building (of reality) is analogous to the study of "Accuracy and Precision" usually taught in introductory numerical methods course. Wikipedia has a very nice explanation - https://en.wikipedia.org/wiki/Accuracy_and_precision Formal Methods help with precision and consistenc…

Thanks! I will make sure to read the last book thoroughly. Have a good day

Re: Formal methods and the future of programming

#122

Post by agentcoops »

arka2147483647 wrote: post #96
nextos wrote: post #60

Earlier quoted context omitted.

I've worked in formal methods for quite a long time, and I disagree a bit with your statement that new logics are not helpful. Industrial logics are really practical and allow you to write all sorts of sophisticated properties that your system should satisfy in a very succinct way. Logic is to computer science and software engineering what calculus is to physics and mechanical or civil engineering [1, 2]. Things like…

> Industrial logics are really practical and allow you to write all sorts of sophisticated properties that your system should satisfy in a very succinct way. It sounds like what you think as positives are exactly the things parent comment thinks as negatives.

I used to work in this field myself long ago (academically and practically). The difficulty that OP didn't suggest much appreciation for is that the interesting spaces for automated verification -- especially of distributed systems, say -- require exploring the space of formalisms between the trivial proofs of propositional logic (SAT solvers) and the undecidable proofs of first or second-order logic (interactive theorem proving environments such as Isabelle and Lean). This is the incredibly large space occupied most importantly by the various modal logics, which allow for quantification over graph traversals. There are remarkably expressive logics where the decision problem remains tractable, such as the modal mu-calculus.

That is, precisely if one wants automated tools for verification the seemingly obtuse work on novel formal systems is necessary.

Re: Formal methods and the future of programming

#123

Post by pfdietz »

jcranmer wrote: post #54
brap wrote: post #15

Whenever I read about formal specs it always seems to me like “write the same tests just in a different way”, or worse, “write the same implementation but in a different way”. I guess doing things twice can help catch errors, but I fail to see what’s so special about formal specs if they can suffer from the exact same bugs as the tests/implementation. I guess the root of the problem is if you want to formally prove t…

There's a famous quote from Dijkstra: "Program testing can be used to show the presence of bugs, but never to show their absence." The flaw of testing is that it can only test the behaviors that you think might be problematic. To actually reach into the category of proactively fixing behaviors that you didn't know could go wrong, you have to reach for more exotic tools in the toolkit. Fuzz testing is a start down thi…

The problem with that mindset is that testing, like verification, becomes extremely powerful as it becomes more automated and you throw more compute at it. And it's arguably easier to automate testing than it is to automate formal verification.

Sure, testing isn't perfect. But is finding 100% of the bugs that much better than finding (say) 99% of them? This is especially the case if the missed bugs tend to be those that happen very rarely.

A formal specification allows automatic generation of tests. So run billions of tests, randomly generated, and see if any violate the specification.

Even theorem proving systems use this sort of thing as a short cut, for example pruning off attempts to prove a universally quantified statement by looking for counterexamples.

Re: Formal methods and the future of programming

#124

Post by ebiederm »

Animats wrote: post #86
ebiederm wrote: post #73

Earlier quoted context omitted.

Have you looked at ADA Spark? If you have does it match your intuition of how things should be done? I am slowly working on something where I hope to integrate such a capability for the things that type systems can't handle quickly. So I would be interested in perspectives of people who have been down this route before.

I've generally liked classic approaches which had entry and exit conditions, and loop invariants, all written using the same syntax and operators as the program. The compiler has to know what to ignore, of course. The compiler should syntax and type check all the proof information, even if it can't verify it. It's important to avoid an impedance mismatch between the proof system and the programming language. If progr…

Thank you. That makes things clearer.

I especially appreciate the trick of asserting the intermediate truth to help the prover along.

As someone who writes software I very much agree that verification of asserts before run time (written in the language itself) is very approachable to a programmer.

In a similar vein I agree with the folks at Jane Street that aiming to rule out specific classes of bugs (as opposed to proving a program is entirely correct) is a very practical goal.

Re: Formal methods and the future of programming

#125

Post by sunshowers »

YetAnotherNick wrote: post #113
nextos wrote: post #60

Earlier quoted context omitted.

I've worked in formal methods for quite a long time, and I disagree a bit with your statement that new logics are not helpful. Industrial logics are really practical and allow you to write all sorts of sophisticated properties that your system should satisfy in a very succinct way. Logic is to computer science and software engineering what calculus is to physics and mechanical or civil engineering [1, 2]. Things like…

> TLA+, which has gained quite a lot of popularity Why do you think that? Outside of just toy examples, and vague examples of "AWS uses that", I don't know of any actual code which has TLA. Most of the things you can do with TLA, you can do with informal math notation quite easily. Do you have any real world long term usage examples?

We have a number of TLA+ models at Oxide. Here's one:

https://github.com/oxidecomputer/omicron/blob/8b0886dbd02229...

Re: Formal methods and the future of programming

#126

Post by ebiederm »

rramadass wrote: post #106
Animats wrote: post #86

Earlier quoted context omitted.

I've generally liked classic approaches which had entry and exit conditions, and loop invariants, all written using the same syntax and operators as the program. The compiler has to know what to ignore, of course. The compiler should syntax and type check all the proof information, even if it can't verify it. It's important to avoid an impedance mismatch between the proof system and the programming language. If progr…

Have you looked at "Verified Design-By-Contract"? See the paper Safe Object-Oriented Software: The Verified Design-By-Contract Paradigm by David Crocker here - https://www.eschertech.com/products/verified_dbc.php David Crocker's Verification Blog - https://critical.eschertech.com/

Not who you asked but I took a quick look.

Typically Design by Contract has meant runtime assertions. I like that they are doing verification before runtime.

At the same time their take on loops (you can't write them and have verification puts me off). Especially when modern c++ has so many prebuilt looks. It would seem to me it should just be a matter of annotating the prebuilt loops and encouraging their use.

I think their approach will fail on modern encryption code because it takes too much control (loops) from the programmer.

Re: Formal methods and the future of programming

#127

Post by rramadass »

ebiederm wrote: post #126
rramadass wrote: post #106

Earlier quoted context omitted.

Have you looked at "Verified Design-By-Contract"? See the paper Safe Object-Oriented Software: The Verified Design-By-Contract Paradigm by David Crocker here - https://www.eschertech.com/products/verified_dbc.php David Crocker's Verification Blog - https://critical.eschertech.com/

Not who you asked but I took a quick look. Typically Design by Contract has meant runtime assertions. I like that they are doing verification before runtime. At the same time their take on loops (you can't write them and have verification puts me off). Especially when modern c++ has so many prebuilt looks. It would seem to me it should just be a matter of annotating the prebuilt loops and encouraging their use. I thi…

Which paper did you read? The "Safe Object-Oriented ..." one that i pointed to or something else? Crocker's writings explain a lot more especially w.r.t. usage with C/C++.

See for example Can C++ be made as safe as SPARK? - https://www.eschertech.com/papers/index.php which identifies a subset and enhances it with annotations. This can be updated with his later article Contracts arrive in C++26! - https://critical.eschertech.com/2025/09/09/contracts-have-ar...

Also see articles under Proving C and C++ programs correct - https://www.eschertech.com/articles/index.php

Animats was bemoaning that OO has declined and that you needed object/DS invariants. I was pointing to the fact DbC has it all (people should always use the runtime checking approach) and with Verified-DbC you could do it statically too. Formal Methods can be done at various levels and a developer can choose and adopt what he feels comfortable with initially before graduating to fullblown heavyweight methodologies/tools. What is needed is developing Formal Method Thinking. See the paper On Formal Methods Thinking in Computer Science Education linked to here - https://news.ycombinator.com/item?id=46298961

Re: Formal methods and the future of programming

#128

Post by rramadass »

nextos wrote: post #60
Animats wrote: post #26

I used to do proof of correctness work, decades ago.[1] We had more proof automation than many of the later systems. The easy stuff was solved by the first SAT solver, the Oppen-Nelson simplifier. The harder stuff used the Boyer-Moore prover, which uses heuristics and previous lemmas to guide the theorem prover. The Boyer-Moore prover had to be helped along by suggesting lemmas, which it would try to prove and which…

I've worked in formal methods for quite a long time, and I disagree a bit with your statement that new logics are not helpful. Industrial logics are really practical and allow you to write all sorts of sophisticated properties that your system should satisfy in a very succinct way. Logic is to computer science and software engineering what calculus is to physics and mechanical or civil engineering [1, 2]. Things like…

Thanks for the pointers to the papers.

One book which seems not that well known is Arindama Singh's Logics for Computer Science 2nd edition - https://www.phindia.com/Books/BookDetail/9789387472433/LOGIC...

For more details see author's webpage - https://home.iitm.ac.in/asingh/books.html

Re: Formal methods and the future of programming

#129

Post by int_19h »

Animats wrote: post #86
ebiederm wrote: post #73

Earlier quoted context omitted.

Have you looked at ADA Spark? If you have does it match your intuition of how things should be done? I am slowly working on something where I hope to integrate such a capability for the things that type systems can't handle quickly. So I would be interested in perspectives of people who have been down this route before.

I've generally liked classic approaches which had entry and exit conditions, and loop invariants, all written using the same syntax and operators as the program. The compiler has to know what to ignore, of course. The compiler should syntax and type check all the proof information, even if it can't verify it. It's important to avoid an impedance mismatch between the proof system and the programming language. If progr…

Rust proc macros are good enough to have design-by-contract implemented in them, although for type invariants it's not exactly ergonomic (because you have to disallow inner mutability to avoid someone grabbing a reference to a field and then mutating it without any invariant checks).

I don't know if there are any solutions combining this with static analysis. Of course, even the runtime checks are very helpful (doubly so in AI-written code).

Post reply on HN