Hacker News Reader

For me the barrier to proving the "hard bits" was never that I couldn't reason about it—I quite enjoyed formal methods in school, and when introduced to them by coworker's who'd done similar—but it was that I didn't have the time to dedicate to learning enough about how to model my problem in a particular new language or system when none of my coworkers were spending such time and my boss wasn't already convinced.

The AI tools are great at lowering the learning curve by changing "how would I possibly express this" to "ah, let's see if this expression of it is actually right?" and "hm, is there a simpler way to express the same thing?"

Like StackOverflow for javascript questions, but for an area that was far to obscure to have a good library of example answers.

I'm not looking to prove the entirety of every system. Usually just some core bits. And often not connected automatically to the code (which may not be gonna change much).

I'm totally with you, but that's not quite what this company and others are trying to do based on their marketing material.

I have long being fascinated by the the field and curious about it on an amature level, i took some basic proof verification and distributed computing classes back in the grad school days, but I'm clearly not an expert in the field by any means. From the article, it seemed like there are plenty of "traps" that i did not even consider - starting from lean hatches like assume(false), expressive power of TLA+ (CTL, ATL), and ofc challenges of tying an real implementation to a proof. To me all three of the above seem challenging enough to deserve their own tools, and i would appreciate smart people putting effort into addressing these rough edges.

Question to you: i can understand how proof verification like z3 or lean requires a special language and an inference engine; given that model checkers like tla+ are mostly about exploring possible program states and checking properties of such states and chains of states, i do not quite understand why it can't be done with a conventional imperative language to express state transitions and invariants - especially an interpreted one like python (esp with continuation support) or a language targeting a vm like wasm where one should be able to snapshot program state?

F-Star and Dijkstra Monads (which are apparently not really monads?) might get you to what you're looking for

The state space you get when using real programming languages like Python is much, much larger than the one you get when abstracting your system design into TLA+. Thus when testing real systems you can only explore very small portions of the state space. This is a real thing people do, although it isn't yet widespread - the term to look for is deterministic simulation testing. Making a DST harness that can handle exploring an application state space without requiring large modification to the application itself is very challenging. Currently Antithesis are the only ones I know who have done it (disclaimer: no connection to this company, I just think they are very cool).

TLA+ is not a model checker. It's a general language for writing mathematics, akin to Lean, only Lean focuses on high mathematics while TLA+ focuses on dynamic systems. There are a proof checker and at least one model checker that work on subsets of TLA+.

As to why TLA+ is better at describing systems than programming languages, the reason is that it's much more general. It can say things like "a routine that sorts in a quadratic number of steps or less" rather than a specific sorting algorithm, and it allows stating (and proving) that a specific sorting algorithm matches that description or not. Most TLA+ formulas are too abstract to be run by a computer (i.e. they describe too many potential algorithms), but that's exactly what makes them useful to describe things when either you don't care about the details or you want to show that a particular algorithm implements a general property.

BTW, even algorithms like Quicksort are, themselves, too general to be accurately described by a programming language (i.e. a language that can be executed). Quicksort doesn't specify how a pivot is chosen (it doesn't matter for the correctness), it doesn't specify how that partitioning is done (ditto), and it doesn't specify in what order the recursion is done or perhaps even in parallel (ditto). Yet a computer needs to be told all these details to run an implementation of Quicksort, even though the algorithm works, and can be proven to work, no matter what these details are. In a language like TLA+ you can say how to choose a pivot or you can say "a pivot is somehow chosen" (which covers all possible mechanisms for choosing one).

Also, TLA+ is much simpler than a programming language and obeys simple and intuitive substitution rules - e.g. `x = 3` is equivalent to `3 = x` and `x = y + 1` is (almost) equivalent to `x - y = 1`, which is what you want when you're after clarity. It's just different from programming languages (because it's maths), so it's a different, though simpler, kind of language to learn.

Have you seen Lampsort?

https://bertrandmeyer.com/2014/12/07/lampsort/

Many languages can do that (Ada SPARK, Dafny, even Java with JML, and quite a few more), but there are really two languages here, the spec language and the program language. The spec language isn't executable, and the program language doesn't spec. What TLA+ does is offer a a single continuum, with a language that's much simpler than both Eiffel's spec language and its program language, and can describe anything at arbitrary precision. It can describe the QS algorithm in general, and it can describe the activations of the logic gates in the CPU as a specific QS runs on a specific machine, and it can take any description of QS, at any level, and show the abstraction/implementation between them. Again, this is all in a language that's much simpler than Python, and that allows reasoning directly in the language because it supports substitution and all the normal manipulation capabilities we expect from mathematical formulas.

> Proving programs correct end-to-end (i.e. code to high-level properties) - as this company and others purport to do - is so difficult that humans have only been able to do it for very small programs (~10KLOC) and even then, in very specialised cases, where the programs have been written in an extra-simple way (often at the cost of performance, because performance often requires more complicated algorithms).

This is not true. It has been done. I’ve seen it done for an entire OS too. Humans are very capable of doing this. The issue is this is seldom done practically speaking because the effort is not worth the benefit when the program becomes too complex.

For simple programs and small domains it’s worth it. For example type checking. Type checking proves one aspect of your program (the types) is fully correct.

> This is not true. It has been done. I’ve seen it done for an entire OS too

That might be what pron's talking about. seL4 is only 10-20K lines of code as far as I remember. Maybe you have another OS in mind, though.

If you're talking about seL4, it is tiny and intentionally simplified. I'm not aware of programs larger than ~10KLOC that have ever been verified end-to-end.

You seem to be implying that it's a toy, which it very much is not.

https://sel4.systems/use.html

I was implying nothing of the sort. It is an important and serious kernel, but a very small one and a very simple one, which it had to be so it could be verified, like the har-realtime safety critical software I worked on and formally verified. We don't yet know how to verify non-small or non-simple software with formal proofs, and unfortunately, the gap in size between the software we can prove and the average software we write has only grown significantly over the past 40 years. If AI knows how to verify "average software", then it certainly doesn't need our help with software tasks that are far simpler. My point was that some companies are imagining an AI that can write software like humans never could and then suggesting they can help it by writing simple software tools.

It isn't a toy for sure, but I doubt that it has good scalability stories when using SMP.. I'd love to be wrong given that even phones are multicores, so feel free to correct me.

It does have SMP support but it's unverified and I'm not sure how widely used or well-tested it is.

> If AI becomes at least an order of magnitude more capable than humans at software development

Doesn't it only need to become an order of magnitude more capable than humans at theorem proving, not general software development?

Maybe (for humans the two often go together), but what's the hypothesis behind assuming it will do the one and not the other? It seems like a very specific and arbitrary bet, not much unlike betting that AI will be able to learn English but not French.

I'm probably being naive here, but with theorem proving, if you have a problem then you can check whether a given solution is correct, letting people make things like AlphaProof, no? I would think that the open-endedness of software development in general would complicate that.

In general, problems whose solutions are easily checkable are not necessarily easily solvable, and the difficulty of finding the proof also depends on how the software is written, which is why humans, at least, don't try to prove arbitrary programs correct, but write the program and the proof together. But regardless, the tools involved are really not very complicated. While it's possible, I find it hard to justify betting on AI being able to prove a 100KLOC-10MLOC program correct while not being able to write a 10KLOC tool well enough.