The biggest problem with Copilot/LLMs is that they effectively operate against anything that programming languages were designed for. What makes programming lan

The biggest problem with Copilot/LLMs is that they effectively operate against anything that programming languages were designed for. What makes programming languages special is that they're well defined, semantically and syntactically rigorous and intended for machine execution. They give us the capacity to formally reason. Instead what we've got now is tools that literally argue with us, rather than anything that actually augments my capacity to reason about, inspect and understand the real performance and hardware of a system my code runs on. What I need is more Coq and less of something that just makes natural language suggestions. What makes a good engineering tool is something that can look at the code right there as it is, use the formal guarantees that programming languages were designed for and give me some verifiably correct suggestions. Not average out 90% of Stackoverflow answers and then hallucinate up some statistical response. Contrast Copilot with tree-sitter. What makes tree-sitter so good as a tool is that it leverages the regularity of programming languages. It can parse and correctly reason about code, instead of relying on some random regex collections and prayers. We've had so many good advances in recent years like the borrow checker in Rust. Why are we going back now and introducing tools that are by design incapable of ensuring correctness? Just to type a little bit faster?