Comment by colechristensen
8 hours ago
I think people are overestimating the usefulness LLMs will bring us based on early examples of low hanging fruit being harvested.
LLMs have a VERY different set of things which are easy and which are hard and from software security to math proofs we're seeing very early impressive results but those will run out and new classes of what is difficult will show themselves.
The "this new tech will cause everything to be easy from now on!" feeling has happened many times before and always new limitations were found.
Industrialization was thought to be basically the end of the need for money or significant labor during the industrial revolution (this optimism is where communism came from) and that future never came.
The same will be here: rapid change but also new limitations which are still hard to imagine.
I program very often in idris2 and I cannot agree more. LLMs tend to take the least effort possible to the point where most of the time, llms are just not useful to program with dependent types. At least, not yet
Have you tried giving them the types you want and then have them auto complete? They are pretty good at a auto completing abstractions
I do but I have no guarantee that the llms will make a sane implementation of the types