Regarding the cost, I’d expect the road to AGI to deliver intermediate technologies that reduce the cost of writing provably secure code. In particular, I’d expect Copilot-like code generation systems to stay close to the leading edge of AI technology, if nothing else then because of their potential to deliver massive economic value.
Imagine some future version of Copilot that, in addition to generating code for you, also proves properties of the generated code. There might be reasons to do that beyond security: the requirement to provide specs and proofs in addition to code might make Copilot-like systems more consistent at generating correct programs.
Regarding the cost, I’d expect the road to AGI to deliver intermediate technologies that reduce the cost of writing provably secure code. In particular, I’d expect Copilot-like code generation systems to stay close to the leading edge of AI technology, if nothing else then because of their potential to deliver massive economic value.
Imagine some future version of Copilot that, in addition to generating code for you, also proves properties of the generated code. There might be reasons to do that beyond security: the requirement to provide specs and proofs in addition to code might make Copilot-like systems more consistent at generating correct programs.