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

101–110 of 129 posts

Re: Formal methods and the future of programming

#101

Post by derdi »

Syzygies wrote: post #24

I nearly adopted OCaml for my current math research, in no small part because of Jane Street contributions. I instead chose Lean 4, as LLMs became able to help code in Lean. I give up a factor of two in performance (a gap likely to close) for what reads to me as the clearest expression of each algorithm. Lean is a beautiful language that makes OCaml read like Old English. Lean is designed to be optionally verified; p…

You are praising Lean for optional verification. They want to add optional verification to OCaml. Where do you see an impedance mismatch? Just in the fact that you don't find OCaml pretty enough?

Re: Formal methods and the future of programming

#102

Post by ajb »

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.

There's a big difference between wanting a succinct proof and wanting a succinct statement of the requirements. The easier it is to state the requirements, the more likely you have stated them correctly. Whereas succinct proof is not relevant for industrial purposes, as long as the proover has a small trusted kernel, it makes no difference to the reliability.

Re: Formal methods and the future of programming

#103

Post by Joker_vD »

____tom____ wrote: post #80
chadgpt3 wrote: post #46

Earlier quoted context omitted.

Non trailing whitespace means the string doesn't end with a space. But foo is a function that converts an AST to a string, that's totally different. Or it's a function that loops until \0 and changes all spaces to + The spec should be a summary of what the impl is supposed to do. You'd want more than just doesn't end with whitespace of course.

> Non trailing whitespace means the string doesn't end with a space No. And this is a great example of the problems with specifications. You still have to write a spec. And this, too, is subject to bugs. What's wrong with the statement above is there are 17 space characters in Unicode and another eight whitespace characters, like newline. If you try to verify that something ends in whitespace, you have to make sure y…

> there are 17 space characters in Unicode and another eight whitespace characters, like newline.

And of course, those 25 characters don't include ZERO WIDTH {SPACE,NON-JOINER,JOINER,NON-BREAKING SPACE} and WORD JOINER, which gives you yet another 5 arguably "it's kinda space, right" codepoints which definitely should not be trailing in any reasonable text string.

Re: Formal methods and the future of programming

#104

Post by bobkb »

addaon wrote: post #72
zahlman wrote: post #67

Earlier quoted context omitted.

> how effective frontier models (ChatGPT-5.5 in particular) are at completing certain manual proofs in the Roqc (né Coq) proof assistant. The proofs aren't always pretty, but ChatGPT can often prove something in minutes and 10 - 100 iterations that would take me, a human who has limited but non-zero proof assistant experience but significant domain experience in the lemmas being proven, much much longer. ... How do y…

With the proof checker.

I assume your idea is, if the spec and the proof is verified the code generated is good enough as well ?

Re: Formal methods and the future of programming

#105

Post by curuinor »

teiferer wrote: post #87
jdw64 wrote: post #3

In other words, because GEN AI a lot of code, the idea is to shift human value toward verification. Sometimes I think about what programming really is. In fact, learning programming itself is a huge challenge for a non English speaker like me. I have to rely on machine translation to understand English documents that have no translation. The materials in my language are about 5 to 6 years behind. Now, since it's impo…

> I have to rely on machine translation to understand English documents that have no translation. The materials in my language are about 5 to 6 years behind. Pretty much off topic, but I strongly recommend you learn English. It takes a little bit of effort, but getting rid of that constant translation overhead will be an enormous boost for you.

guy's korean, looks like? korean english is the hardest language pair of two industrialized-nation languages, almost.

Re: Formal methods and the future of programming

#106

Post by rramadass »

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…

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/

Re: Formal methods and the future of programming

#107

Post by rramadass »

jdw64 wrote: post #3

In other words, because GEN AI a lot of code, the idea is to shift human value toward verification. Sometimes I think about what programming really is. In fact, learning programming itself is a huge challenge for a non English speaker like me. I have to rely on machine translation to understand English documents that have no translation. The materials in my language are about 5 to 6 years behind. Now, since it's impo…

Your ideas about Formal Methods are not clear nor quite correct.

Read first the paper On Formal Methods Thinking in Computer Science Education to understand the different levels of practice available. Here is a previous comment of mine which explains and links to the paper - https://news.ycombinator.com/item?id=46298961

Carroll Morgan just published his Formal Methods, Informally: How to Write Programs That Work which teaches you how to think in a formal method manner before you start using the heavyweight tools - https://www.cambridge.org/highereducation/books/formal-metho...

Also read Understanding Formal Methods by Jean-Francois Monin to get an overview of some of the tools and the concepts/mathematics embodied in those tools.

With just the basic ideas from the above viz. Set Theory, Predicate Calculus, learning to think of a Program as a trajectory through a state space, you can start enforcing the trajectory using simple asserts(i.e. predicates) for preconditions/postconditions/invariants. Now because of Curry-Howard Isomorphism (https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...) you can treat "propositions/formulae as types" and thus exploit the type system itself as constraints enforcing the above trajectory.

Once the above is grokked, you can move on to more complex logics (eg. FOL/HOL/Temporal/Separation etc.) and learn about tools/methodologies which implement them (eg. Alloy/B-Method/TLA+ etc.).

Finally, with AI tools, the threshold for the practice of formal methods has dramatically come down. This enables one to do Formal Specification and Verification with guaranteed traceability for AI-generated code which IMO is a necessity.

Re: Formal methods and the future of programming

#108

Post by jmalicki »

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…

"Logic is to computer science and software engineering what calculus is to ... mechanical or civil engineering"

Things professionals rarely use in practice?

Re: Formal methods and the future of programming

#109

Post by ____tom____ »

Joker_vD wrote: post #103
____tom____ wrote: post #80

Earlier quoted context omitted.

> Non trailing whitespace means the string doesn't end with a space No. And this is a great example of the problems with specifications. You still have to write a spec. And this, too, is subject to bugs. What's wrong with the statement above is there are 17 space characters in Unicode and another eight whitespace characters, like newline. If you try to verify that something ends in whitespace, you have to make sure y…

> there are 17 space characters in Unicode and another eight whitespace characters, like newline. And of course, those 25 characters don't include ZERO WIDTH {SPACE,NON-JOINER,JOINER,NON-BREAKING SPACE} and WORD JOINER, which gives you yet another 5 arguably "it's kinda space, right" codepoints which definitely should not be trailing in any reasonable text string.

Unicode never ceases to amaze me.

Re: Formal methods and the future of programming

#110

Post by addaon »

bobkb wrote: post #104
addaon wrote: post #72

Earlier quoted context omitted.

With the proof checker.

I assume your idea is, if the spec and the proof is verified the code generated is good enough as well ?

Today, I write the code. It’s trivial and takes a lot less time than writing the spec, and since I’m using conventional tooling for WCET and stack sizing it’s nice to get those right up front. The LLMs sometimes tweak the code slightly for provability, but this is usually either direct operator replacement (shift with multiplication, and with modulus, etc) or factoring out a block to a function to tie a contract onto it, both of which I trust my compiler to undo (simple arithmetic operations and inlining, respectively) with zero to minimal impact on the generated binary.
Post reply on HN