Post #4139031

2026-07-27 14:08 UTC

@agl@infosec.exchange To be frank, dependently-typed languages have always been interesting and we have had the machine help us write the code long before GenAI/LLMs became 'de jour'. The devil appears with writing your initial theorems not when asking the machines to provide proofs. The old mantra still exists: Garbage in; Garbage out. Bad propositions in; Bad proofs out.

Replies (1)

@agl@infosec.exchange 2026-07-27 14:21

@jfdm@discuss.systems I’m familiar with old school tactic automation, and have even attended a summer school on F*. I believe that the LLM world really does improve the automation drastically on what we had before. You may very well be correct that things still don’t work out. I can see a bunch of ways that it still goes wrong when trying to use something like Lean for quotidian software engineering. To give one example, perhaps we find that, with much more detailed interfaces, we just can’t compose things. The detailed interfaces were previously implicit, so you could ignore the mismatch and bumble along. I.e. maybe that wasn’t the problem, but actually a critical part of how things sort of manage to work. That would be a depressing outcome! I think we haven’t really explored this in normal contexts. I feel that the overhead of these languages previously precluded their use in all but specialised domains. Now that the overhead is much less, I think it’s an interesting avenue to explore. But certainly not a guaranteed success.

Open ##4139030