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

41–50 of 129 posts

Re: Formal methods and the future of programming

#41

Post by [deleted] »

brap wrote: post #37
jlebar wrote: post #18

Earlier quoted context omitted.

> 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”. [...] Can anyone enlighten me? A big difference is that formal methods allow you to use the "for all" quantifier. For example, you might write a unit test that says "foo('abc') returns a string with no trailing whitespace". But with formal me…

>Of course, you have to define what "has the same behavior as" means And that's really my issue, for example when you define "has no trailing whitespace", you are basically writing a piece of the implementation. Cover all behaviors, and you have basically re-implemented the function, no? In other words, if I have the full formal spec of f(), isn't that the same thing as having f()?

[deleted]

Re: Formal methods and the future of programming

#42

Post by IshKebab »

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…

That can definitely be a problem, and I have definitely written formal specs (for hardware in SVA) where I'm like "I'm just implementing this again". And actually that's a totally valid formal verification task to do - formal equivalence checking of an implementation against a model (which is just another implementation). I can feel (and sometimes is) tautological.

However you usually try to not do that. If possible (and it usually is possible) your formal spec will be either:

1. Another implementation, but a much simpler one. For example you can formally verify the equivalence of a pipelined dual issue CPU, with a combinatorial single cycle model.

2. More general properties that much be true about the implemention, rather than exactly what the implementation must be. The classic example is compression: decompress(compress(x)) == x.

Re: Formal methods and the future of programming

#43

Post by pydry »

bluGill wrote: post #40
brap wrote: post #37

Earlier quoted context omitted.

>Of course, you have to define what "has the same behavior as" means And that's really my issue, for example when you define "has no trailing whitespace", you are basically writing a piece of the implementation. Cover all behaviors, and you have basically re-implemented the function, no? In other words, if I have the full formal spec of f(), isn't that the same thing as having f()?

> In other words, if I have the full formal spec of f(), isn't that the same thing as having f()? In some cases, however quite often, the spec is much simpler. For instance, it's easy to say that after running sort on some list, that the result is sorted. However, it is very hard to come up with the algorithm to do that from the specification. Sometimes that is even a point. Bubble sort, quick sort, tim sort, we can…

I did some of this stuff in college and what bugged me was that the spec actually ended up more complex than the code and it had bugs.

That was a long time ago and they said that formal methods were the future back then, too.

Re: Formal methods and the future of programming

#44

Post by brap »

bluGill wrote: post #40
brap wrote: post #37

Earlier quoted context omitted.

>Of course, you have to define what "has the same behavior as" means And that's really my issue, for example when you define "has no trailing whitespace", you are basically writing a piece of the implementation. Cover all behaviors, and you have basically re-implemented the function, no? In other words, if I have the full formal spec of f(), isn't that the same thing as having f()?

> In other words, if I have the full formal spec of f(), isn't that the same thing as having f()? In some cases, however quite often, the spec is much simpler. For instance, it's easy to say that after running sort on some list, that the result is sorted. However, it is very hard to come up with the algorithm to do that from the specification. Sometimes that is even a point. Bubble sort, quick sort, tim sort, we can…

This makes a lot of sense, thank you!

Re: Formal methods and the future of programming

#45

Post by chadgpt3 »

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…

For trivial functions they can be. Function: isPrime. Impl: loop to sqrt(n) and check divisibility. Spec: returns true if nothing divides. Impl: return true at the end if we didn't return false.

It's not exactly the same because your spec says nothing divides, not just up to sqrt(n). It's definitely not a test if you do it right.

Re: Formal methods and the future of programming

#46

Post by chadgpt3 »

brap wrote: post #37
jlebar wrote: post #18

Earlier quoted context omitted.

> 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”. [...] Can anyone enlighten me? A big difference is that formal methods allow you to use the "for all" quantifier. For example, you might write a unit test that says "foo('abc') returns a string with no trailing whitespace". But with formal me…

>Of course, you have to define what "has the same behavior as" means And that's really my issue, for example when you define "has no trailing whitespace", you are basically writing a piece of the implementation. Cover all behaviors, and you have basically re-implemented the function, no? In other words, if I have the full formal spec of f(), isn't that the same thing as having f()?

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.

Re: Formal methods and the future of programming

#47

Post by chadgpt3 »

pydry wrote: post #43
bluGill wrote: post #40

Earlier quoted context omitted.

> In other words, if I have the full formal spec of f(), isn't that the same thing as having f()? In some cases, however quite often, the spec is much simpler. For instance, it's easy to say that after running sort on some list, that the result is sorted. However, it is very hard to come up with the algorithm to do that from the specification. Sometimes that is even a point. Bubble sort, quick sort, tim sort, we can…

I did some of this stuff in college and what bugged me was that the spec actually ended up more complex than the code and it had bugs. That was a long time ago and they said that formal methods were the future back then, too.

It's possible for that to happen but probably means either the function is too trivial or you're missing some abstraction in the spec

Re: Formal methods and the future of programming

#48

Post by winwang »

Love this. I've shifted in the past few months to using highly expressive types in Scala 3 to have types carry more and more compile-time proofs (without macros, though a couple are warranted). Not only does it help with agentic test "sprawl", it seems to prevent agents from falling into lower-quality modes of operation. One of the more annoying things I've been preventing is what I call "noun accretion", where agents try and make a new monomorphic type for everything, instead of clearly genericizing when sensible. My bet is on formal-method-shaped tooling (including languages with strong type systems) to accelerate decent-quality agentic coding.

When I say "highly expressive types", I mean techniques I'd likely not want to ship in a typical codebase, unless the team was already on the typelevel programming bandwagon (i.e. having HKT and type functions being basic blocks already, not weird). Agents are better at "math" than basically most devs (even category-theory-pilled ones), at least in terms of knowledge. Better yet, they are decent at pedagogy, especially when considering they have "infinite" patience for dialogue.

In a more personal setting, I've had Codex Lean-ify a couple of my hobby proofs, it was extremely easy. Note: not saying it did this 100% "correctly" (gotta learn more Lean 4 to check more thoroughly), but it also seems to check for classic proof gotchas by default. Very excited for the future of formal methods.

Re: Formal methods and the future of programming

#49

Post by ngruhn »

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 want to do offensive programming (I coined that term). You take risks, but you fix things quickly and ship.

Nice, I like the term too. But the paradigm is absolutely status quo in the industry. The thing is: with Gen AI the cost of "defensive programming" has gone way down, while the cost of (human) verification has gone way up. On the other hand, formal methods make verification cheap but come with massive implementation overhead (writing specs, types, proofs, and generally bending the implementation into a rigid framework). But Gen AI can automate all that laborious work. It's a match made in heaven.

Re: Formal methods and the future of programming

#50

Post by cadamsdotcom »

I’ve had huge success with TDD and nothing more formal than that; test frameworks are great for verifying “business correctness”. But they can also verify other aspects - eg. asserting that 3 queries ran instead of 103 for a request, to prove absence of N+1 queries.

Really any technique that lets the agent create its own verification is ideal, as it makes verification scale.

Post reply on HN