I agree. It’s especially weird moving across related domains because suddenly something you think you know has changed meaning. For instance eBPF is “verified”, but the verification is almost completely unrelated from the usual connotations.
You cannot escape from the human verifying the properties you want verified mechanically. This only gives you leverage in specific scenarios where specification is much simpler than the implementation.
I think the point I wanted to make was that even if it was deterministic (which you can technically make it to be I guess?) you still shouldn’t live in a world where you’re guided by the “guesses” that the model makes when solidifying your intent into concrete code. Discounting hallucinations (I know this a is a big preconception, I’m trying to make the argument from a disadvantaged point again), I think you need a stronger argument than determinism in the discussion against someone who claims they can write in English, no reason for code anymore; which is what I tried to make here. I get your point that I might be taking the discussion to seriously though.
The Maryland one (that would be me, although I haven’t really done anything except the WASM bindings, this is really all Joomy’s work, kudos to him) is vacationing in Izmir right now, why would that even be important though?
I'll add some links for the original VGD paper and related articles, that should help in short term. Thank you! I'll look into writing something on VGD itself in the next few weeks.