Coq typeclass resolution is Turing-complete | Hacker News Reader

Coq typeclass resolution is Turing-complete

thaliaarchi.github.io

90 pointsthaliaarchi24 comments

Author here! I had a hunch that the typeclass resolution engine in the Coq typechecker could be Turing-complete, so I proved it by implementing a variant of Brainfuck in it. Feedback welcome.

Not a feedback, question. How do you feel doing work like this in a world where people see javascript as a acceptable language? Second, somewhat related, what would be the biggest problem preventing wide, industry adoption of Coq/other formal methods?

I think there are varying levels of assurance that developers need while writing software. I tend towards stricter languages with more guarantees, like Rust with its borrow checker and Coq with its powerful types and proofs. This doesn't need to be a universal preference, though; my preferred work is in compilers, which requires a high degree of assurance, and I study programming languages formally.

The largest barrier to greater adoption of languages like Coq with proof systems built-in is the formal background needed to get started. I think that Rust has done an excellent job at making stronger systems more accessible, but it takes a lot of conscious work.

With JavaScript, I think the idea that performance in language design can be an afterthought, made up for by world-class optimizing JIT compilers, is fundamentally wrong. It doesn't give users a meaningful way to easily reason about the performance of the programs they write. The main implementation of Python, pythonc, is essentially an interpreter over an unoptimized bytecode format, giving it poor performance. I think performance considerations should be a fundamental part of the language design.

Thanks for your perspective.

I'm wondering how this squares with the tendency of formal language theory folks to push for functional languages. It's clearly a preferred approach if rigorous correctness is your main goal, but don't functional languages like Haskell suffer from the fundamental issue that reasoning about runtime performance is really hard?

Haskell is notoriously difficult to reason about runtime performance, but that is due to its lazy evaluation, not because it is functional. Lazy evaluation can cause hidden space leaks, where expressions have not yet been evaluated, so maintain references to other values. Most functional programming languages are not lazy.

Yeah I've wondered about that. Especially the obsession with singly linked lists.

> The largest barrier to greater adoption of languages like Coq with proof systems built-in is the formal background needed to get started.

I believe this to be a language problem and not a conceptual problem. All that you need to pragmatically formalize semantics is Hoare triples and basic predicate calculus[1]. Anyone that can understand an if statement already has the necessary conceptual machinery. The so-called “formal methods” community delights in over complicating the problem with gadgets like category theory. Which is ironic, because they’re introducing the same kind of unnecessary complexity that causes the problem that they’re trying to solve.

[1] ok that’s not utterly strictly true because arrays (or mutable functions, as I like to think of them) present some subtleties, but those are more a problem for the definers rather than the users.

I was referring to how the communities of these languages typically frame the problem, so you need formal background to read the materials published on it. As you say, this is a major barrier. This is where Rust shines, in that they've framed the language in terms of how its used, developed accessible documentation, and steered away from delving into the theory behind it.

I don't think people find Javascript an acceptable language. The meteoric rise of TypeScript proves that.

I have met and seen online a lot of people that see no problems with vanilla Javascript. I honestly don't even know where to begin here.

I’m shocked you didn’t just start with white space. ;)

I’m excited to dig through this more. Nice work!

How does the famous largest number contest winner loader.c fit into this? Its search for well typed programs has to be halting...

I was not familiar with loader.c, so I did some digging[0]. It implements the Calculus of Constructions, which Coq is based upon, and generates all programs encoded lower than some value. The search is halting, though very long.

From the analysis[1] in the contest:

> {loader.c}, diagonalizes over the Huet-Coquand `calculus of constructions'. This is a highly polymorphic lambda calculus such that every well-formed term in the calculus is strongly normalizing; or, to put it another way, a relatively powerful programming language which has the property that every well-formed program in the language terminates. The program's main function is called D. … D works approximately as follows: given an argument x, it iterates over all bit strings with binary value less than or equal to x, and, if such a bit string codes for a well-formed program (`term' in lambda-calculus language), it runs the program (`strongly normalizes the term' in lambda-calculus language.) The return value of D is then obtained by packaging together the return values of all these programs. The program's return value is D@@5(99).

[0]: https://googology.fandom.com/wiki/Loader%27s_number

[1]: http://djm.cc/bignum-results.txt

I'm sick of making another CRUD app. Do you have suggestion if I want to do something like this for a living ?

The use of proof tools in software is very, very interesting but still a niche application because of the relative specialization of the programmer and the need: most software limps by just fine with shockingly high defect rates. But, of the folks I know that do this kind of work you’re looking at critical applications in the MiC or bigger tech companies that produce their own hardware. Compilers for Important Things also fit the profile. I’m not aware of apprenticeship models. More education or building provably correct systems on your own time until you can go professional are the roads I’ve seen (but not traveled). Model checking distributed algorithms and complex systems is another path, one I suspect has more industry need than is realized. Getting over the imagination hump in an org is the trick there, yet.

I hope by the time I retire proof tools are the norm. It’s heading in that direction, seems to me. When I started my career static vs dynamic was a big deal and here we are with typescript being mainstream. I do a lot of work in Rust and what that compiler can prove about lifetimes is still sometimes a surprise, compared to what I used to just have to muddle through over in my mind.

> I’m not aware of apprenticeship models.

Maybe not a popular answer, but I think the answer to this is grad school. Someone gets a PhD in an area like this (e.g., building either theorem provers or their related infrastructure), then gets a job in the same or an adjacent area after graduation.

That's not the only way to do it, but looking around in my area of research (compilers and programming languages for HPC) there are definitely many more people who do it this way than just figure it out on their own.

Learn Haskell and join a company/team/etc that is cool about it. Gotta watch out though - there's a growing cohort of Haskellers out there focusing on appeasing management by putting down advanced stuff by saying such people are "easily distracted by shiny ideas."

Definitely some uncool ones out there, but Haskelldom is large so you can definitely find a place that at least allows for advanced type stuff but is still normal software dev. That may scratch that Coq itch.

But Coq is strongly normalizing… it always halts. What gives?

This is the automatic resolution of some instance satisfying a typeclass constraint, and is not related to the termination of functions. This does not call a function. If you compare it to the relational definition I give at the end of the semantics section, the typechecker does not similarly infer satisfying constructers for the relation. Proof tactics can also diverge, but that's different.

Typeclass resolution is implemented as a layer of automation that is above the type-checking kernel, so much like with nonterminating tactics, if it doesn't halt you mostly just end up with confusing automation that doesn't help you prove something, but you shouldn't be able to prove false. Mostly it's a usability nightmare for typeclasses, and in the case of this post also a way for hilarity to ensue.

> Mostly it's a usability nightmare for typeclasses

And also for Rust traits, C++ templates, etc (those are all nonterminating)

(Conflating a few things here, and only noticing now; there are also languages with undecidable type checking in which one cannot prove false, mostly because of fancy equality checking, though that's undesirable in some ways. But it's not accurate to think of typeclass resolution as part of the type checker IMO. It is in a layer similar to tactics.)

It just gives up after running for too long as any Turing-complete type checkers are doing.

Any practical consequences?

Reply on news.ycombinator.com