I have seen demos of Idris where just the type signature itself allows for automatic function implementation, which is very cool and almost magical. And you ar

I have seen demos of Idris where just the type signature itself allows for automatic function implementation, which is very cool and almost magical. And you are probably right that many of the trivial cases can perhaps be guessed by some AI — but I think in these cases a simple, more deterministic algorithm could also find a match, iterating through a few proving strategies (I believe this is how the aforementioned idris demo worked). What might have resulted in your downvote (I didn’t downvote your comment, I think it adds to the discussion!) is that many people are tired of the over-hype of LLMs, and taken your comment blindly as support of that. With that said, I do think that you overestimate the capabilities of LLMs, as my go to example: they can’t solve even Sudokus. And any other similar, “recursive” thought is simply fundamentally impossible by LLMs in a single step. It is also the barrier in the popularity of dependently types languages - it is easy to give a proof of List::head. Database::connect on the other hand goes through multiple layers of the whole stack, and function proofs do not compose — two trivial to prove functions composition might be impossible to prove, e.g. I can compose 2 such functions and get some unsolved math problem of your choice.