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 pr

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.