khealer's blog

proof assistants
By khealer, history, 2 years ago, In English

Hello,

Have any of you tried the proof assistants (lean, coq etc)? Is it applicable to the problems of the site?

thank you

  • Vote: I like it
  • +11
  • Vote: I do not like it

Comments Comments (4)
| Write comment?
»
2 years ago, # |
  Vote: I like it 0 Vote: I do not like it

I actually wrote a short blog, using CP problems as an introduction to Coq. Coq in particular has an extraction mechanism that allows you to prove a function correct according to a specification, and then extract it into a Ocaml/Haskell program you can submit to CF and most judges.

Now doing so in-contest is not really useful/feasible. Also, I don't think proof assistants like Coq or Lean are well-suited for reasoning about imperative programs; there are some languages like Dafny that might be more appropriate for that.

→ Reply
  • »
    »
    2 years ago, # ^ |
      Vote: I like it 0 Vote: I do not like it

    I didn't imagine to use it during a contest ^^ I was going for lean, do you think that coq is more suitable? The coq code is much less readable than lean....

    → Reply
    • »
      »
      »
      2 years ago, # ^ |
        Vote: I like it 0 Vote: I do not like it

      I'm not sure exactly what your goal is, but IMO the two are fairly similar.

      → Reply
»
2 years ago, # |
  Vote: I like it 0 Vote: I do not like it

It's hard going. But it's worth giving a try. I'm working on CoqCP, a repository of formalized CP proofs. No running programs yet, but there will be some. The repository is still in its early stages. I want the repository to be bigger and cover more CP problems. It would take me a lot of practice to be able to use the technology in contest, but I'm working to get there.

→ Reply