Eisenberg articulates a future where Artificial Intelligence (AI) fundamentally shifts the programmer's role but does not eliminate the need for precise languages. He claims:
- The future division of labor involves humans focusing on precise specification (intent) while AI handles the implementation (code generation)
- He proposes using advanced type systems (specifically dependent types) as the "specification language". The compiler then acts as the "verifier", proving the AI's code matches the human's spec.
- Future languages must be verbose and explicit enough for humans to verify the AI's output easily.
Interestingly, Eisenberg also admits that "writing a precise specification is hard" and "humans are lazy". His conclusion that dependent types are the solution to AI correctness may be a "golden hammer" fallacy. Personally, I rather think that we will be able to give semi-formal instructions to the LLM exactly the same way as we write functional and performance specifications as engineers to design and implement complex systems. The LLM or AI agent will be able to translate those semi-formal specifications, which respresent the intent, not the solution, to a formal specification system (such as e.g. Event-B) and also conduct all the proofs and finally generate corresponding (C or Ada, or even assembler or machine) code. The LLM will also be able to back-translate the formal specification to human language, so the human can verify, whether his/her intents are properly reflected. See https://rochuskeller.substack.com/p/why-rust-solves-a-proble... for more details about this.
Rochus•1w ago
- The future division of labor involves humans focusing on precise specification (intent) while AI handles the implementation (code generation)
- He proposes using advanced type systems (specifically dependent types) as the "specification language". The compiler then acts as the "verifier", proving the AI's code matches the human's spec.
- Future languages must be verbose and explicit enough for humans to verify the AI's output easily.
Interestingly, Eisenberg also admits that "writing a precise specification is hard" and "humans are lazy". His conclusion that dependent types are the solution to AI correctness may be a "golden hammer" fallacy. Personally, I rather think that we will be able to give semi-formal instructions to the LLM exactly the same way as we write functional and performance specifications as engineers to design and implement complex systems. The LLM or AI agent will be able to translate those semi-formal specifications, which respresent the intent, not the solution, to a formal specification system (such as e.g. Event-B) and also conduct all the proofs and finally generate corresponding (C or Ada, or even assembler or machine) code. The LLM will also be able to back-translate the formal specification to human language, so the human can verify, whether his/her intents are properly reflected. See https://rochuskeller.substack.com/p/why-rust-solves-a-proble... for more details about this.