I was reading about proof assistants, formal verification etc, also I have a lambda calculus implementation. My question is: Is it possible to prove that my implementation is correct?

In fact I have two implementations, having a single proof for both would be nice but I have no idea how to attack the problem. What I know is that all possible inputs are infinite, but, the rules of lambda calculus are finite. Can I implement only the sets that verify that these rule are holding and this way prove that the whole implementation is correct?

  • 1
    $\begingroup$ I don't understand what you're asking. You say you've read about formal verification and are wondering if you can prove that your implementation is correct? That's exactly what formal verification does. What have you been reading? I'm wondering if maybe spending some more time on research would be useful. $\endgroup$
    – D.W.
    Jun 28 at 3:12
  • $\begingroup$ I don't understand what you're saying when you say "all possible inputs are infinite". Normally every input to an algorithm has finite length. I don't understand what is meant by "implement only the sets...". We're a question-and-answer site, so we require you to be able to articulate a focused, understandable question. $\endgroup$
    – D.W.
    Jun 28 at 3:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.