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

111–117 of 117 posts

Re: We have proof automation now

#111

Post by monarchwadia »

Proof automation will make things a lot easier. I'm not entirely sure that it's the only thing required, but it's a big part of the thing required.

What's more interesting to me is, how do we prove that the business intent is accurately encoded in the code? This is a different problem. Not "is the logic internally coherent," but "is the logic going to give us what we want?"

And how do we make sure that the logic keeps giving us what we want, iteration after iteration?

I've open source a tool, Drift, for this purpose. So far, biased and anecdotally as its builder, this has been the missing layer. It works because the spec is treated as a duplicate of the code, written and committed in the repo and kept in sync with hashes. The LLM then checks for diffs manually. There are ways to use perplexity here as well. Here is an article about how to get started. https://monarchwadia.medium.com/how-to-make-your-agent-more-...

Doubtless, many more automations will come. We live in very exciting times. It has been a while since a new technology affected every corner of software engineering with such depth of change. This might be unprecedented.

Re: We have proof automation now

#112

Post by m1el »

nickpsecurity wrote: post #91
m1el wrote: post #27

Self-insert time. I spent some time exploring this topic. Here's my thesis: Formal verification was expensive. 20x expensive compared to just developing the software, as the author notes. The cost of finding and developing exploits also was high. That creates an incentive to put software verification aside, since it solves a relatively small problem, at an extremely high cost. We've seen how Mythos has found more vul…

There were many prototyoes of certifying compilers and proof-carrying code in academia. The FLINT group by themselves had many. Maybe try building on those.

Thank you for the suggestion, I will be sure to learn from those!

Re: We have proof automation now

#113

Post by dleink »

rafaelRiv wrote: post #100
vatsachak wrote: post #95

Earlier quoted context omitted.

Have you tried giving them the types you want and then have them auto complete? They are pretty good at a auto completing abstractions

I do but I have no guarantee that the llms will make a sane implementation of the types

You still want to write/review/refine the types yourself.

Re: We have proof automation now

#114

Post by whoke »

vessenes wrote: post #78

I think it's worth putting a Knuth quote up on your board when you think about verification as an end goal: "Beware of bugs in the above code; I have only proved it correct, not tried it." Or, as Wolfram proposes in another link on the front page today, the irreducibility of computation means we cannot generally get all bugs out of systems. To my mind, one of the risks of going all in on verification is that you just…

I like the concept of "inevitable grittiness"! I think languages like Lean actually do a very nice job of pushing the grittiness out to the boundaries of your program. Everything else can stay pure, and in domains that are amenable to mathematical reasoning (compilers, DSP, etc) it feels like a natural fit. I don't think you have to go all in, either. I ported the compiler project I'm working on from TypeScript to Lean and recently spent a weekend making all the functions total and implementing a few basic theorems. On a basic level it feels like writing Haskell, but there's a lot more room to grow with it.

Re: We have proof automation now

#115

Post by m1el »

makira wrote: post #97
m1el wrote: post #27

Self-insert time. I spent some time exploring this topic. Here's my thesis: Formal verification was expensive. 20x expensive compared to just developing the software, as the author notes. The cost of finding and developing exploits also was high. That creates an incentive to put software verification aside, since it solves a relatively small problem, at an extremely high cost. We've seen how Mythos has found more vul…

This is great! Not sure which high level language you are targetting, but consider Subrust instead of C: https://github.com/orbitalhigh/subrust How does LowIRSSA compare to P1pp from boot2 ?

LowIRSSA is very different from the SSA in the repo.

LowIRSSA looks way more like SSA-WASM than assembly

Re: We have proof automation now

#116

Post by trenchgun »

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 did write small programs myself, but mostly with Claude Code. It was very pleasant to work in it with Claude Code. Implemented a shell and 40 of coreutils. Did not really get very far with proving properties of them, but had working programs. Reading Lean4 is pretty nice. Nicer to read than OCaml, almost as nice as Haskell.

Re: We have proof automation now

#117

Post by nlogn_alltheway »

I just feel an existential angst, are we damned to keep reinventing the same wheel?

Static contracts and proofs are basically solved for industrial use in SPARK, yet somehow we keep reinventing. Is computer science really engineering? We don’t stand on the shoulders of giants, every new generation has the urge to invent a leave a mark. This in itself is great, except that, in contrast to other branches of engineering (say mechanical, or structural) previous know how is ignored and disregarded. Perhaps there is too much of it, and SNR these days is too low, impossible to be held in one’s head. Perhaps it’s easier these days with LLMs to survey what’s done. Yet the slop waves keep crashing on us.

We have seen this with dbs. The relational model layed the foundations. Yet periodically a new craze emerges. Everyone’s chases the latest cool new thing, until the ugly warts that were know to be there decades ago resurface and become real blockers (looking at you mongo).

Yet another post about program proofs, yet no mention of the only industrial strength, actually practical and pleasant to use formal verification language: SPARK.

Post reply on HN