|
|
|
|
|
by nborwankar
1057 days ago
|
|
I have a fundamental disagreement about the premise that abstraction from CPU instructions should be the basis of a language model. I posit that the starting point should be lambda calculus which is formally equivalent to Turing machine based theories.
Lambda calculus -> functional languages -> algebraic type aware languages (Haskell?) -> languages used in theorem proving (Agda ?..) is a progression that allows logic and provably correct programs and reasoning about programs.
Messy natural language can be used as away to collect requirements by an LLM that can translate them into formally correct tests and specifications which can be used to Instruction-train LLM’s that could (insert frenetic hand waving here) write provably correct (or close) code in say Haskell or Agda.
In summary Lambda Calculus is a better starting point because it’s logically closer to formal languages and reasoning. |
|