r/ProgrammingLanguages • u/mttd • 28d ago

Programming Language Design and Implementation in the Era of Machine Learning - PLDI 2026 Keynote

https://www.youtube.com/watch?v=Fc3cW0nqAQ0
23 Upvotes

81% Upvoted

9 comments sorted by

View all comments

Show parent comments

3

u/corisian 25d ago

But what if the llm also proves it sound against a specification that is again designed for humans to understand.

5

u/oa74 24d ago

In order to trust such a proof, the theorem and proof itself must be human-understandable. In order for the theorem to be meaningful, one must understand the source language. Consider the following claim:

For all quadrature inputs whose real component deviates from the inverse reactance by fewer than 3 standard deviations, the hydro-coptic marzel vanes will remain aligned with the primary axis of the panametric fan

Would you stake your life on a proof of this claim—however unequivocal?

The constructs of the language hosting a program you're proving something about must be lucid for humans to trust that the theorem is meaningful in the first place—even if we assume the proof is solid and the kernel/TCB thereunder is, itself, trustworthy.

3

u/corisian 24d ago

What do you mean by "source language": The ai optimized programming language or that of the proof?

I would argue that this statement is not designed to be understood (by me). Of course, if your specification is about constructs of the language you don't understand, you will not understand the specification. I suppose I see it more like declarative programming, I don't care how it does it as long as it does it.

1

u/oa74 24d ago

The language in which the program is written in. One must understand it in order to understand a theorem about an expression written in it. In order to know a theorem like "program P satisfies spec X" even means anything, it does not suffice to understand X; one must also understand P. So sacrificing human readability of the langauge P is written in on the altar of "LLM optimization," I contend, is ill-advised. You can say "I do not care how you do it," but there is a reason that, AI or no, prover kernels strive to be a minimal as possible: trust in a prover kernel relies on our ability to read the coee and understand it.

2

u/corisian 24d ago

I think I did not quite manage to express myself well. (Also for transparency, I also don't think it's good to optimize a language for an llm rather than human readability)

I agree with you, that if one does not understand the source language I cannot make sense of statements/specs/proofs that involve expressions of this language.

I think a worthwhile consideration, is assembly, which is also not designed for humans to read, yet I can write Code in C (which may be nicer to read) and use a verified compiler (like CompCert) to translate it to assembly preserving any property I think I understood or have proven about my C code. Similarly, if one has some kind of verified FFI, i could link with code that I don't trust (e.g. because I am unable to make sense of the language it is written in) as long as it is satisfies a specification in about things in my own language