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

We have proof automation now

imperialviolet.org

Post reply on HN
Print view View original

101–110 of 117 posts

Re: We have proof automation now

#101

Post by penteract »

el_pollo_diablo wrote: post #45

I have already written it, and I will write it again: dependent types and total functions do not scale. Maintenance is terrible. Suppose that you have managed to write a non-trivial piece of software with dependent types encoding all sorts of properties everywhere. The actual computation and proof are intermingled. Think of the author's innocent bound-check proof in the zstd decoder, but across the whole program, wit…

> dependent types and total functions do not scale.

I'm not convinced that this is much more true than the claim "correct code doesn't scale". If you add to your code in a way depends on a new property for correctness, and the code was not previously written with awareness that the new property was necessary, then you need to check through the rest of your code and make sure that the property is maintained. Formally verifying things is painful because it actually makes you check this.

Instead, we live in a world where we use software that is not completely correct. Browsers have remote code execution vulnerabilities because people who make browsers decided it's more important that javascript can run quickly, and that new standards get implemented, than that we avoid such vulnerabilities at all costs.

Re: We have proof automation now

#103

Post by momentoftop »

let_rec wrote: post #63
momentoftop wrote: post #35

Theorem provers have always made extensive use of AI and automation. Formal logic is insanely laborious, and it took Russell a monumental effort to not get very far with his manual verifications in Principia Mathematica, working out all the details by hand. In 1956, Newell came up with the Logic Theorist which was able to prove a decent chunk of the Principia automatically. When Newell informed him, Russell conceded…

To someone completely outside the field: why is creating a formal verification of an existing proof so hard? 1. Convert the natural language proof steps into formal language 2. Pass it to the solver to verify the steps Genuinely curious!

Converting natural language steps to a formal language isn't too challenging. But basically none of those steps will follow directly from the previous steps by any primitive deduction rule of any formal system. From the perspective of formal logic, there are massive gaps in the reasoning, and these need to be filled to pass the verifier. And they are absolutely massive, so massive that it would be completely intractable to fill them in manually.

That's where most of the tech in a theorem prover exists: its tooling to automatically fill in the gaps so your proof can pass the verifier. The tools and automation here are genuinely great, but you still end up having to write way more steps and inferences than you'd see in any maths textbook, and the details are far more fiddly because the formal verification is not very forgiving.

As an illustration, consider how you get from:

  X = (x + y)(z + w)
to

  X = xz + xw + yz + yw
The second equation doesn't follow directly from the first in any logical system. Instead, it follows by the distributive law, commutativity and associativity of addition, commutativity of multiplication, symmetry and transitivity of equality, and you'll need to have some means to specialise these universal statements and reason about term substitution.

A modern prover will do simple algebra like this for you, but the tooling had to be built to do it. In other domains, the tooling just dies trying to connect what an average working mathematician or even a mathematics undergraduate would consider obvious, and you're stuck either having to elaborate massive tedium, manually guiding the automation, or having to write new bespoke tooling to fill the gaps.

Re: We have proof automation now

#104

Post by gugagore »

el_pollo_diablo wrote: post #45

I have already written it, and I will write it again: dependent types and total functions do not scale. Maintenance is terrible. Suppose that you have managed to write a non-trivial piece of software with dependent types encoding all sorts of properties everywhere. The actual computation and proof are intermingled. Think of the author's innocent bound-check proof in the zstd decoder, but across the whole program, wit…

> they encourage grouping everything that concerns a value ("put this value in a dependent type that encodes everything known about it")

I understood you to be saying "bundling is encouraged", in the sense of

https://leanprover-community.github.io/glossary.html#bundled...

I'm not sure it's encouraged. I agree that it felt natural to define a type like NonNegativeInteger, or a wrapper type like `Sorted(T)` to indicate that that wrapped list is sorted. But I think this is an area of style and aesthetic that is still emerging, far from ossified.

The problem of "threading" new things within existing programs is an important one to address, and it has multiple solutions (context management, dynamic scoping (lol), implicit arguments, type classes). I am curious if the claim of "does not scale" is mitigated by one of those solutions...

Re: We have proof automation now

#105

Post by chrisjj »

andai wrote: post #66

I had a funny experience recently, during a vibe coding bender. This was a few weeks ago when these very impressive new models came out, a whole new class of intelligence and autonomy! So I wanted to see how far I would get, letting the computer handle all the details. Eventually I did take a look at all the new code, and found that one of the main features had been implemented completely backwards, in a way that was…

> An LLM also pointed that out, so I guess it must have been a different one which implemented it?

Or the same one a minute later. LLMs are the software equivalent of Patagonian weather.

Re: We have proof automation now

#106

Post by armchairhacker »

el_pollo_diablo wrote: post #45

I have already written it, and I will write it again: dependent types and total functions do not scale. Maintenance is terrible. Suppose that you have managed to write a non-trivial piece of software with dependent types encoding all sorts of properties everywhere. The actual computation and proof are intermingled. Think of the author's innocent bound-check proof in the zstd decoder, but across the whole program, wit…

The key is to structure the program so that only a tiny trusted core is verified but the properties extend to untrusted code. For example, the sel4 microkernel is formally proven to not crash (barring hardware), so any program running on it will not crash the entire computer, just itself. Or (only parts of it are formally verified, but) the Rust borrow checker practically guarantees any Rust code without `unsafe` will not produce memory errors; any amount of lines of Rust code, without any proofs themselves, are covered by the relatively tiny trusted core that is the borrow checker.

Re: We have proof automation now

#107

Post by [deleted] »

logicchains wrote: post #46
anilgulecha wrote: post #40

I'm convinced Math is the canary for what's going to happen to knowledge work. Coding was ahead in harnessing early LLM capability, but Math, given it's pure form, has aleady racing ahead. The dimensions to notice are: Research speedup, practitioner expertize, labour dynamics, junior entrants, world impact. In that sense it's a canary, whatever happens to Math, will in order flow to other sciences in-order of purity:…

Math is the opposite of a canary because it's possible to generate infinite amounts of synthetic training data for it, unlike almost every other kind of knowledge work where correctness depends on external input.

[deleted]

Re: We have proof automation now

#108

Post by nextos »

saithound wrote: post #74
codebje wrote: post #7

Earlier quoted context omitted.

IMO the biggest issue was always not knowing what correct is in the first place. The vast majority of software we use, the stuff that's riddled with errors, has those errors largely because what it's supposed to do is vague and never, ever deals with edge cases. You can't formally verify your application works correctly under transient network error conditions if you never thought about what your application should d…

> . You can't formally verify your application works correctly under transient network error conditions if you never thought about what your application should do under those conditions. [..] it's expensive to spend that much time thinking through it all, when users are largely trained to just accept crashes, glitches, inconsistencies, and the occasional sprinkle of data loss. Indeed. The last bug I fixed in a produc…

> You can't formally verify your application works correctly under transient network error conditions if you never thought about what your application should do under those conditions.

This is why it's so important to separate functional from stateful code. Functional code is generally easier to specify. And, by isolating stateful code, one can e.g. fail fast and avoid stepping into undefined behavior.

Re: We have proof automation now

#109

Post by ndriscoll »

singularity2001 wrote: post #64
trenchgun wrote: post #48

Earlier quoted context omitted.

Lean4 is a general purpose programming language.

Have you tried writing any programs in it?

I don't see why it would be particularly difficult beyond not already having a lot of IO libraries (like Kafka connectors or whatever). Pure functional programming in Scala with IO monads is quite pleasant.

Re: We have proof automation now

#110

Post by andai »

chrisjj wrote: post #105
andai wrote: post #66

I had a funny experience recently, during a vibe coding bender. This was a few weeks ago when these very impressive new models came out, a whole new class of intelligence and autonomy! So I wanted to see how far I would get, letting the computer handle all the details. Eventually I did take a look at all the new code, and found that one of the main features had been implemented completely backwards, in a way that was…

> An LLM also pointed that out, so I guess it must have been a different one which implemented it? Or the same one a minute later. LLMs are the software equivalent of Patagonian weather.

Yeah that's a great point. In OpenRouter's model fusion article found that just running Opus twice (and combining the results) gave similar results to one Fable on a research task, because there is so much variability in what it does every time you run it, and web research tasks benefit from that variability.

(Unfortunately it also took twice as long and cost twice as much as Fable, but that's besides the point :)

Post reply on HN