khealer's blog

proof assistants
By khealer, history, 21 month(s) 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?
»
21 month(s) 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
  • »
    »
    21 month(s) 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
    • »
      »
      »
      21 month(s) 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
»
21 month(s) 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