3 ms·

Prediction: as agentic code generation gets better, more and more code will be written JIT for it to be executed for security reasons. The engineer of the futur

Prediction: as agentic code generation gets better, more and more code will be written JIT for it to be executed for security reasons. The engineer of the future is not only the one who uses agents to code, he uses agents to code each time "the" program is ran.

p-e-w 1mo ago
I doubt it. It seems far more likely that such code will be written just once by LLMs, but in a way that allows its claimed guarantees to be formally verified (e.g. in Lean). At that point there’s no need to JIT an implementation each time.
- TacticalCoder 1mo ago
  My bet is one ultra-hardened, minimal, front-facing system which does N-modular redundancy which N systems, each written on a different stack/different language. The hardened software picks the computation that wins the majority. It's not an issue to write all the implementations in the various stacks/languages: we'll have better and better LLMs to help us. This shall bring security and shall allow to detect shitload of bugs (both in the implementation itself but also in the stack). Heck, this could even be compatible with GP: one of the implementation could be JIT'e by a LLM, others could be written in advance (and Lean formally verified). Not sure which sense it'd make though. I'm 99.9% sure it's coming for if it's not, I'll make one.
  - fc417fc802 1mo ago
    I feel like that idea is erroneously mixing concepts. You want quorum in safety critical contexts, generally to guard against hardware failure. I think using independent implementations in such a scenario is uncommon and to date largely a stop gap to save money by replacing formal verification. For security formal verification is really what you need. Both of the software and also eventually the hardware, since typically formal verification of software won't hold up against something like rowhammer. (Although TBF I'm not sure what sort of formal verification would have caught rowhammer.)
mihaelm 1mo ago
What's there to gain security-wise? Nondeterministic generation & then execution of that code without proper verification seems to be the opposite of a good security posture.
- daishi55 1mo ago
  why are you assuming there would be no proper verification in this scenario?
  - compounding_it 1mo ago
    Because the verification would also be done by something non deterministic and then that’s a paradox.
    - daishi55 1mo ago
      Feed the LLM output into a “deterministic” verifier, problem solved. That’s how LLMs verify their new mathematical proofs with lean.
  - mihaelm 1mo ago
    Proper verification would be deterministic rules the JIT-ed code would be checked against, so it would have to be non-JIT. Since the comment is talking about using more & more JIT for security reasons, I assumed it extended to verification too. I don't get why you'd generally switch to JIT for security reasons.
    - patmorgan23 1mo ago
      Who writes the formal verification spec and when?
      - daishi55 1mo ago
        I suspect there are already plenty of test suites out there for something as universal as a networking stack.
dakolli 1mo ago
No
psd1 1mo ago
Humanity is a Type I civilisation. It has energy constraints. AI coding runs at hundreds of watts, and more capable agents consume more. That is paid, today, from capex, provided by the biggest bubble in human history. I can deliver your fantasy by running a space heater while i download a docker image.

p-e-w 1mo ago

I doubt it. It seems far more likely that such code will be written just once by LLMs, but in a way that allows its claimed guarantees to be formally verified (e.g. in Lean). At that point there’s no need to JIT an implementation each time.

TacticalCoder 1mo ago
My bet is one ultra-hardened, minimal, front-facing system which does N-modular redundancy which N systems, each written on a different stack/different language. The hardened software picks the computation that wins the majority. It's not an issue to write all the implementations in the various stacks/languages: we'll have better and better LLMs to help us. This shall bring security and shall allow to detect shitload of bugs (both in the implementation itself but also in the stack). Heck, this could even be compatible with GP: one of the implementation could be JIT'e by a LLM, others could be written in advance (and Lean formally verified). Not sure which sense it'd make though. I'm 99.9% sure it's coming for if it's not, I'll make one.
- fc417fc802 1mo ago
  I feel like that idea is erroneously mixing concepts. You want quorum in safety critical contexts, generally to guard against hardware failure. I think using independent implementations in such a scenario is uncommon and to date largely a stop gap to save money by replacing formal verification. For security formal verification is really what you need. Both of the software and also eventually the hardware, since typically formal verification of software won't hold up against something like rowhammer. (Although TBF I'm not sure what sort of formal verification would have caught rowhammer.)

mihaelm 1mo ago

What's there to gain security-wise? Nondeterministic generation & then execution of that code without proper verification seems to be the opposite of a good security posture.

daishi55 1mo ago
why are you assuming there would be no proper verification in this scenario?
- compounding_it 1mo ago
  Because the verification would also be done by something non deterministic and then that’s a paradox.
  - daishi55 1mo ago
    Feed the LLM output into a “deterministic” verifier, problem solved. That’s how LLMs verify their new mathematical proofs with lean.
- mihaelm 1mo ago
  Proper verification would be deterministic rules the JIT-ed code would be checked against, so it would have to be non-JIT. Since the comment is talking about using more & more JIT for security reasons, I assumed it extended to verification too. I don't get why you'd generally switch to JIT for security reasons.
  - patmorgan23 1mo ago
    Who writes the formal verification spec and when?
    - daishi55 1mo ago
      I suspect there are already plenty of test suites out there for something as universal as a networking stack.

dakolli 1mo ago

psd1 1mo ago

Humanity is a Type I civilisation. It has energy constraints. AI coding runs at hundreds of watts, and more capable agents consume more. That is paid, today, from capex, provided by the biggest bubble in human history. I can deliver your fantasy by running a space heater while i download a docker image.