31–33 of 33 posts
Anyone have ideas as to why this works so well with JavaScript specifically? I tried to include similar commands in Python (i.e., use a prompt that implies Python based on commenting style) and it doesn't even write code, but instead keeps adding new comments.
Earlier quoted context omitted.
>in favor of fast but potentially wrong or insecure results. Formal methods don't eliminate wrong or insecure results. Formal methods tell you that a program matches the specification when certain conditions are true eg. no bit flips, the computer does not crash, the kernel doesn't kill your process, that allocations succeed, that your program can make progress (the kernel can decide to never schedule your program),…
> Formal methods don't eliminate wrong or insecure results. Yes, they do. That's the entire purpose of a proof. Of course formal methods cannot prevent or even detect wrong specifications, but that's no different from generated code either. > Using formal methods slows you down compared to things like testing which can get us most of the way there in less time. But that's the point - formal methods are slow if people…
A wrong specification can give you a wrong or insecure result. That was my point. Formal methods aren't a sliver bullet and your system still needs to be robust to failures.
>so why not add the step and create a hybrid system that verifies the generated result?
Because the time spent writing a specification is time wasted if there ends up being no issues with the generated code.
Interesting how you still need to have some intuitive sense of what's going on under the hood. (You can't say "make Zelda," you have to ask for an array of symbols and manipulate them.) In that sense it feels like this is still programming, but at a higher level of abstraction with a weird fuzzy compiler. Now we can go from natural language -> JavaScript -> assembly etc. rather than just the last two. Mediocre progra…