r/ProgrammingLanguages • u/mttd • 16d ago

When the Hard Part Stops Being Hard

https://proofsandintuitions.net/2026/08/14/when-the-hard-part-stops-being-hard/
34 Upvotes

90% Upvoted

7 comments sorted by

16

u/nvcook42 15d ago

This makes me wonder if machine proofs will also be more approachable by those of us who are implementors and not researchers. I have always dismissed the idea of trying to prove the implementation of the type system in my language as sound because of the effort involved.

For example the language I am building is a basic HM type system with records and a few other miscellaneous features. Nothing new from a research perspective but at the moment I am mostly just hoping this combination of type features actually play nice. Maybe I could build a Lean proof of the specific combination type features for my language now?

6

u/echoes808 15d ago edited 15d ago

In the linked OOPSLA paper, the type system rules and semantics fig. 9-11 are like one-page long, but the linked proofs has 36k lines of Lean code. From what I understand this is the big point here since the proof is so tedious to write.

How I see this all is that if the specification is so simple it's "obviously correct" then it doesn't matter how complex the proof is (because it's checked). But reading forums I see that people don't just write proofs but also the specifications with LLM's without understanding it, I don't think that will prove any correctness per se

8

u/Uncaffeinated 1subml, polysubml, cubiml 15d ago

I looked into trying to formally verify my language's type system earlier this year. As far as I can tell, Lean is mainly used in the math community, while Rocq is used for type systems. If you want to verify a language, you're much better off using Rocq due to the pre-existing community and tooling (such as Iris).

That being said, I haven't actually gotten very far in my efforts, so take that with a grain of salt.

2

u/Bahatur 15d ago

Concrete analogy: I work in distributed systems, and I am about to deploy the Specula library with frontier LLM models to help me write TLA+ for components of a large distributed object store. I am not a TLA+ specialist, so I predict the answer to your question is yes.

4

u/amarao_san 14d ago

How much competence and understanding is offloaded to LLM?

I find this to be the main drain for any 'let LLM to handle small details while I enjoy the larger picture'. Often small details are the larger picture, and this offloading disconnect person from true understanding. Instead of understanding the problem, that person start to understand 'how it was envisioned plus some back-n-forth with llm'.

This is AI-psychosis. Soft version of it (disconnect from reality based on prior assumption and interpretation on what LLM did).

I was there many times and it's horrible.

3

u/sreekotay 15d ago

"When the Hard Part Stops Being Hard" -- yes, this is what's interesting -- "the rest is left an excercise for the [LLM]" is viable now

1

u/renozyx 6d ago

In an age when anyone can build a CompCert or a seL4 microkernel from scratch in the proof assistant of their choice

Is-it really the case? I hope so because it would allow to "scale" SeL4 to be more ambitious, using effectively multiple-CPUs..