| IMHO and IME, we need new programming language(s). I started on Pascal and C/C++. Then I moved to Python. It freed my mind from types, and I was able to think more high-level about the data structures. After another decade and half, I discovered Haskell. Turns out the types were not the problem; the lack of proper type inference was. So it turned out to be a usability issue of C/C++. Writing type explicitly everywhere is just bad UX. My point is this. LLM's allow you to program and reason about code in a natural language. It clearly has some advantages over programming in traditional programming languages. But it has a significant disadvantage that natural language is not semantically sound. (And as a result, you get what people incorrectly call indeterminism of LLMs.) I believe we need better programming language in which we can also express metalogical properties of programs, as if we expressed them in natural language, but with soundness guarantees. This new language would then become the new source code. This language needs to have primitives for fuzzy and modal logic, and there need to be some algorithm that can typecheck (check if the statement is consistent) and type-infer (if the statement is inconsistent or ambigous, fill-in the likely parts, possibly interactively). We know such a formal system must exists, because a very close variant of it has already been implemented (or discovered?) within LLM. We essentially need to discover true metaprogramming - writing programs that manipulate programs. From Curry-Howard isomorphism, we know there is analogy between program execution and reasoning. So it is time to start using same language for both. (I am looking into using Triage Calculus for this.) |