apantykhin (Jun 19 2020 at 07:58): apantykhin (Jun 19 2020 at 07:58):Hello! I'm newbie in COQ and auto synthesis of programs by proofs.
TLDR: What is the application of program made from theorem proof?
I have a questions about understanding. What is value of programs transformed from the theorem proof? As I understand, such kind of programs is good that they proof theorem by existing of self. Theorems just make relationships between different properties of theory, right?
For nowI see only one real application: define functions, make some lemmas for proof some properties of definitions and then generate program. Something like Proof Driven Development.
Karl Palmskog (Jun 19 2020 at 08:16):in many cases in computer science, the structure of the correctness proof of a function can follow the structure of the function, which saves effort and guides its development. See for example here where all the wildcards _ in a program definition are proof obligations later filled by tactics.
Last updated: Oct 13 2024 at 01:02 UTC