@screwlisp LOL, I hope my “responsible use of AI” comments didn’t offend the regular audience members too badly! I wasn’t able to see the chat at the time.

Like @someodd said, and I agree, you can use LLMs for type checking, and possible also for producing heuristics that guide a sat-solver. For example, LLMs are already being used to find zero-day vulnerabilities by both attackers and defenders. As another example, using an LLM in a place similar to where you would use refinement types with a sat-solver can work as long as you have a classical type checking algorithm to guide your explorations of the design space.

LLMs are an algorithm like any other: they can be overused and abused (e.g. slop coding), they can be used by bad people to harm good people, but these algorithms do have legitimate uses. And with more research, like what we see happening in China right now, the energy cost of these algorithms may drop quite a bit in the near future, so at least the problem of data centers destroying the planet and using up all the fresh water could theoretically be resolved.

I hope soon the hype around LLMs will die away, and people will stop seeing these things as proto-gods and start seeing them as just another tool you can use to solve certain specific software engineering problems.

@dougmerritt @havoc @mdhughes