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

91–100 of 129 posts

Re: Formal methods and the future of programming

#91

Post by ____tom____ »

codebje wrote: post #88
____tom____ wrote: post #81

Earlier quoted context omitted.

Exactly. You can prove that f(a,b) always returns a+b. And then you overflow the int on that machine. Oops.

I am not sure that the perspective you have taken is the same as what I understood from the parent post; what I took from it is that things like registers, memory locations, ways to implement square root, and so on, are all _implementation choices_ that are not important properties of the specification. You specify that the hypotenuse is the square root of the sum of squares, but whether square root is implemented us…

Perhaps I have misunderstood or was unclear.

Everything the parent comment mentioned were implementation details that did not affect the correctness of the code.

I just wanted to point out that there are implementation details that DO affect the correctness of the code.

And, of course programs need to run on multiple architectures. So it's hard to do what people seemed to be talking about in this thread and verify code just from the source code.

If you have the luxury of proving the correctness of the CPU, compiler and OS, that should be a big win. Otherwise, it seems to just be another type of testing. Still useful, but calling it verified or proven seems a bit much.

From my perspective, it seems more to be writing another, more complicated program, with more opportunities for bugs, and seeing if the results agree

Re: Formal methods and the future of programming

#92

Post by Joker_vD »

____tom____ wrote: post #81
nemo1618 wrote: post #62

Earlier quoted context omitted.

I think the key is that, while you may think you have a full formal spec of f(), you actually do not. You have a program written in some language, and that language has its own spec, and the language is compiled to asm which has its own spec, and the asm executes on an architecture that has its own spec, and so on. So when you write a function like: func hypot(x, y): return sqrt(x*x + y*y) You might think you have "f…

Exactly. You can prove that f(a,b) always returns a+b. And then you overflow the int on that machine. Oops.

Well, ideally you proof should've failed because your axioms should be aware that arithmetic operators in the programming language of your choice are operating modulo some large power of two, and thus don't produce correct results for some particular inputs.

Admittedly, this one peeves a lot. Remember when Java's binary search and mergesort (and implementations in many other languages' standard libraries) turned out to have a bug of this kind [0]? Admittedly, the proof was informal, but if you are trying to prove some properties of a program X written in a certain programming language Y, you can't "just assume" that the semantics of Y are different from what they are, right? The integers do overflow in Java, that's explicitly stated in the Java's spec... and that means that a lot of even the most simplistic code has some very non-obvious correctness preconditions, which most of the times, I believe, are simply hoped to be true.

[0] https://research.google/blog/extra-extra-read-all-about-it-n...

Re: Formal methods and the future of programming

#93

Post by seqradev »

We are working toward applying formal methods from the application security testing side, but I believe the same kind of approach can be applied to business logic verification as well. For that, we are using the taint analysis technique — a fairly well-established formal methods approach, but still not widely applied in the field because of the complexity of dataflows in real codebases.

Scaling formal methods beyond AST pattern matching and some simple type checking turns out to be a really hard task! It took years of research and development to reach the point where taint analysis enables us to trace interprocedural dataflows in real codebases in minutes and find deeply hidden vulnerabilities.

If this sounds interesting to you, take a look at our project: https://github.com/seqra/opentaint

Re: Formal methods and the future of programming

#94

Post by rendaw »

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…

The same with unit tests, they're best suited for problems where the specification is much simpler than the implementation. A sorting algorithm can be long and complicated, but a unit test just needs to present unordered input and assert that the output matches ordered output. A sorting algorithm is also well suited for formal verification.

If you're rewriting the implementation, I think it's probably not a good use for unit tests or formal verification.

As another commenter said, unlike unit tests which cover a specific case, and where you need multiple tests for edge cases and both positive and negative results, formal verification will cover all cases.

Re: Formal methods and the future of programming

#95

Post by akoboldfrying »

Veserv wrote: post #13
jnwatson wrote: post #6

Earlier quoted context omitted.

The general idea is that formal methods are self-verifying, up to a point. Sloppy formal methods simply won't prove. The point up to which formal methods stops is: do the formally encoded requirements actually encode what I want to be true? One can make the argument that the requirements is a much smaller surface to verify than that of the entire program. The counter argument is that figuring out what you want the pr…

> One can make the argument that the requirements is a much smaller surface to verify than that of the entire program. This argument is unfortunately empirically false for any program of any meaningful complexity (>1000 lines, probably even as low as >100 lines ignoring well-defined algorithms and data structures) using current formal methods. Complete formal specifications are usually multiple times larger than the…

> Complete formal specifications are usually multiple times larger than the corresponding source code and encode esoteric propertys necessary for the proof, but which are largely even more impenetrable than a undocumented codebase.

Is it possible that the spec could be factorised into something higher-level and more modular? If not, can you give a flavour of the type of unavoidable esoteric detail? (One area I can see lots of complications is when dealing with versioned data, especially in multiple interacting systems -- naively, correctness needs to be proven for every combination of versions, even if some are never seen.)

Re: Formal methods and the future of programming

#96

Post by arka2147483647 »

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…

> 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.

Re: Formal methods and the future of programming

#97

Post by red75prime »

zahlman wrote: post #67
addaon wrote: post #38

I've been playing with related ideas recently, and can talk about them at length... but one thing that's surprised me is just 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-…

> 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…

Proof checkers fuel the AI hype by outputting "valid" for a hallucinated text. /s

Re: Formal methods and the future of programming

#98

Post by blueblazin »

As someone with a bit of interest in programming languages (design and implementation) this was really interesting to me:

> For most people who work on programming languages, the easy part is coming up with new and better ideas about how to make programming better. The hard part is convincing anyone to actually use those ideas for real work.

Totally agree, there's only so much strangeness you can introduce in a new language[1] regardless of benefit.

But AI agents should not feel much resistance to radically new ideas in PL design. I've been thinking for a while now about how PL design will evolve post agentic AI. I think it will be very interesting to see what new ideas we can come up with to improve programming languages when we worry much less about adoption.

[1] https://steveklabnik.com/writing/the-language-strangeness-bu...

Re: Formal methods and the future of programming

#99

Post by brainless »

I am not a language nerd but I keep on experimenting in my own ways to use the type system to generate code that is more reliable.

I build a coding agent specifically for small models, which makes everything harder. I started this chat with Claude to build the next step: https://claude.ai/share/4264e5f6-b334-426c-afe4-904d233ef946 - how can I go from PRD to a typed representation of the business logic.

The I started building as per https://github.com/brainless/nocodo/blob/feature/praxis_agen.... The praxis crate: https://github.com/brainless/nocodo/tree/feature/praxis_agen... and a sample Todo app: https://github.com/brainless/nocodo_example_todo_app

Generating unit tests for the library functions of any project would be done via a separate agent than the one coding the functions. And then use tree-sitter to statically check code to PRD (provenance graph).

Again, not a language nerd, just enjoying chasing a goal.

Re: Formal methods and the future of programming

#100

Post by gottlobflegel »

reinitctxoffset wrote: post #17

I caught the religion on using types in conjunction with LLMs about eighteen months ago, but I only really got serious about `lean4` like six to eight months ago and now I wouldn't even consider using AI assist in software work with a `CIC` proof substrate that has practical C/C++ (and therefore, everything) FFI. We've banned everything from JSON to Python, rewritten `nix` to have a compiler, and almost everything we…

Listing Agda and Idris 2 under CIC makes your lambda hierarchy diagram misleading at best.
Post reply on HN