Блог пользователя khealer

proof assistants
Автор khealer, история, 15 месяцев назад, По-английски

Hello,

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

thank you

  • Проголосовать: нравится
  • +11
  • Проголосовать: не нравится

»
15 месяцев назад, # |
  Проголосовать: нравится 0 Проголосовать: не нравится

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.

→ Ответить
  • »
    »
    15 месяцев назад, # ^ |
      Проголосовать: нравится 0 Проголосовать: не нравится

    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....

    → Ответить
    • »
      »
      »
      15 месяцев назад, # ^ |
        Проголосовать: нравится 0 Проголосовать: не нравится

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

      → Ответить
»
15 месяцев назад, # |
  Проголосовать: нравится 0 Проголосовать: не нравится

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.

→ Ответить