> I also thought about pushing more toward Lean and theorem proving instead of a lighter SMT-style direction
I think your intuition here is good. For these settings I think you want formal methods that are highly automated.
Question about your calculator example: is the intended use case that the user would write these L0-L2 files? Or is it expected that an LLM would write them with user intervention? And the go program, how is that obtained from L2? Is that a symbolic transformation or is the LLM doing it?
Apologies if this is written somewhere and my skimming missed it.
I think your intuition here is good. For these settings I think you want formal methods that are highly automated.
Question about your calculator example: is the intended use case that the user would write these L0-L2 files? Or is it expected that an LLM would write them with user intervention? And the go program, how is that obtained from L2? Is that a symbolic transformation or is the LLM doing it?
Apologies if this is written somewhere and my skimming missed it.