4 ms·

I like there is us who like formal methods and guarantees of correctness for our code. And then there are the others who now generate approximately code with l

I like there is us who like formal methods and guarantees of correctness for our code. And then there are the others who now generate approximately code with large language models that mostly runs. They are winning.

cgio 4y ago
It’s a repeat of search & hope/trust (Google) vs define and query (semantic web) and yes they are winning and will win. Fine tuning your scope for extreme accuracy might be less efficient a strategy than fine tuning your loader for extreme speed
- mcguire 4y ago
  In most situations, a half-assed answer quickly will a beat a good answer slowly. Most. ""Software should be reliable."" Reliability is not usually worth the effort. Most software is not used enough, or not important enough, to make any effort worthwhile. In almost all systems, errors are created at every step and propagate through the system routinely without causing problems.
specialist 4y ago
Ship early, ship often. First to ship wins. Flood the zone. Often phrased as "worse is better." Like, hypothetically, imagine you spent two whole weeks designing and implementing a new programming language, which was guaranteed to be installed on millions of computers overnight. Any language which took three weeks to finish, like wasting a week testing, would be DOA. Like how the (brood parasite) cuckoo chick hatches early and then murders all the other chicks.
intrepidhero 4y ago
But when the robot uprising comes our killbots will be unstoppable terminators and their killbots will explode the first time they encounter a set of stairs.
nextos 4y ago
When the latest incarnation of ChatGPT was out, I had the same thought. However, I then became convinced there might be some synergy between both. Imagine a programming system where you can specify little components using Hoare or Separation Logic, i.e. pre/postconditions. An engineer could spend his effort specifying little components, but code and proof generation can be handled by GPT. Actually, many tasks can be offloaded to a SAT/SMT solver. Lots of verification and synthesis efforts already do the last bit, offloading to SAT/SMT solver. This would be a win-win. Formal methods would become cheaper to use, and software would become built using rigorous engineering.

cgio 4y ago

It’s a repeat of search & hope/trust (Google) vs define and query (semantic web) and yes they are winning and will win. Fine tuning your scope for extreme accuracy might be less efficient a strategy than fine tuning your loader for extreme speed

mcguire 4y ago
In most situations, a half-assed answer quickly will a beat a good answer slowly. Most. ""Software should be reliable."" Reliability is not usually worth the effort. Most software is not used enough, or not important enough, to make any effort worthwhile. In almost all systems, errors are created at every step and propagate through the system routinely without causing problems.

specialist 4y ago

Ship early, ship often. First to ship wins. Flood the zone. Often phrased as "worse is better." Like, hypothetically, imagine you spent two whole weeks designing and implementing a new programming language, which was guaranteed to be installed on millions of computers overnight. Any language which took three weeks to finish, like wasting a week testing, would be DOA. Like how the (brood parasite) cuckoo chick hatches early and then murders all the other chicks.

intrepidhero 4y ago

But when the robot uprising comes our killbots will be unstoppable terminators and their killbots will explode the first time they encounter a set of stairs.

nextos 4y ago

When the latest incarnation of ChatGPT was out, I had the same thought. However, I then became convinced there might be some synergy between both. Imagine a programming system where you can specify little components using Hoare or Separation Logic, i.e. pre/postconditions. An engineer could spend his effort specifying little components, but code and proof generation can be handled by GPT. Actually, many tasks can be offloaded to a SAT/SMT solver. Lots of verification and synthesis efforts already do the last bit, offloading to SAT/SMT solver. This would be a win-win. Formal methods would become cheaper to use, and software would become built using rigorous engineering.