Coding models are running out of data 🧵 The ability of LLMs to code depends heavily on the data they see about code, and lately the industry seems to have consumed essentially all high-quality code data for training and evaluation. Progress is visibly slowing. Whoever finds the next big pool of data holds the key to a new door. My group came from programming languages and formal methods, and we know where such a pool is. More than that, we believe this data changes what an AI answer is: code should ship with its specification and a machine-checked proof, so we no longer need to spend the human time to review the code itself. We call this new paradigm intent computing, and we ran several experiments...