3 ms·
There's some software where it's important not to have bugs and know exactly what it does, and some where any attempt to specify what it's supposed to be doing,
by staunton 3y ago
There's some software where it's important not to have bugs and know exactly what it does, and some where any attempt to specify what it's supposed to be doing, let alone fixing all the bugs, is a waste of time. (And things in between...)
Currently, a lot of instances of the first situation get the treatment befitting the second. This is because it's still too hard to use these tools at scale. However, the trend is certainly towards improving tooling and the cost of doing this will go down a lot.
Maybe in a hundred years programming will be replaced by either "formally specify what you want", if you know what you want, (AI fills in implementation of how it does what you want, as well as a proof that it does) or, if you only very roughly know what you want, explain it to the chatbot and answer it's questions.
- deleted 3y ago[deleted]
- seanmcdirmid 3y agoAI probably disrupts programming in the next couple of decades, where they produce not only software but static and dynamic validation artifacts of correctness. It’s sad though, I would have really liked to see how human programming could improve with better tooling, it seems like a lot of formal specification work (and program synthesis using such) could be improvised with just better user interfaces.
- rgmerk 3y agoSo the AI spat out code and a formal spec and a theorem prover spat out a proof that the code is consistent with the formal spec? Great. Does the formal spec represent a complete and accurate description of what the code is supposed to do? shrugs
- seanmcdirmid 3y agoIf an LML can write an essay that humans can read, surely it’s conceivable that it could spit out proofs/tests/docs etc…in a human readable form. So really, you can just decide for yourself then.
- rgmerk 3y agoSo really, you can just decide for yourself then Even if you can understand what the proof proves (not a given) do you personally understand the actual requirements for the software perfectly?
- seanmcdirmid 3y agoBuilding software is a conversation right? Your specification starts out vague, the AI makes a bunch of assumptions, and then you just say “oh, I really didn’t want that”, wash rinse and repeat.
- smaudet 3y agoI'm not convinced this is adequate, your specifications will be come rather unweildy. If you employed this approach, I would want to pair it at a minimum with a test suite. Even then, how do you know that your system (covered by hill climbing suites of tests that pass), has correct behavior for all things you didn't specify? You don't. Better to build from the ground up formally than fight with "AI" that probably got it worse than wrong first try.
- seanmcdirmid 3y agoYou don’t anyways now. You just have some assurance, not total assurance, with current practices. Many people will find something conversational (in that you have some documentation about what it did and can correct assumptions) good enough because it brings close enough to the human status quo. I hope your pessimism is founded though, I would really like to see programming by human advance rather than the whole thing be taken over by AI. Hybrid approaches are also possible (AI in the loop but not in the core position).
- cvoss 3y agoIn the general case, the "write the spec and the AI does the rest" boils down to automated theorem proving, and I'm optimistic AIs will get pretty good at this in a lot of useful situations. Even today, in limited well-defined problem spaces, there are sometimes good algorithms for this sort of thing. See Dana Angluin's algorithm for learning the DFA that recognizes a regular language given through an interactive process of having the user provide examples/counterexamples, which serve to provide an increasingly constrained spec.