Post #4139030

@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.