New language request: Coq

[proger]

What programming language should we add?
Coq

What is the official website for the language?
https://coq.inria.fr/

Is this a language that comes in many variants? If so, which variant should we support?
The official coq 8.6 is good.

Is there a testing framework available for the language?
If it compiles — it works :)

Who will be leading the effort to launch the track?
me (@proger) and @vzaliva

<3

[kytrinyx]

Welcome 🌻

If it compiles — it works :)

If it compiles it runs, but that doesn't say anything about whether the program has the desired functionality. Is there a way to provide a specification? All of the exercise implementations in Exercism rely on unit tests as the specification.

[proger]

In our case the spec could look like a type (quite literally) for which the person who does the exercise just needs to fill in the program.

Here's the example of an exercise we're getting inspiration from: https://www.cis.upenn.edu/~bcpierce/sf/current/Basics.html#lab38

Would this work?

[vzaliva]

Another idea is to use modules. We can provide Module interface with list of things to prove/implement. User will provide module implementation. The unit test will instantiate the module.

[kytrinyx]

I think so.

/cc @jtigger @parkerl Would you help think about this? @ErikSchierboom I'd be curious to hear your thoughts as well.

[vzaliva]

Here is what I have in mind:

1. Examples may need some "set-up": types and definitions. (important point these are not necessarily transparent. Some exercises may ask to prove properties of particular implementation).
2. We would like to enforce interface (type) of user's solution.
3. At the unit test part in addition to ensuring that user provided all required lemmas or definitions, we may do additional tests, for example using Compute.

My current thinking is to use module types to enforce the interface. I started to experimenting with few sample problems using this approach. Here is my current code: https://github.com/vzaliva/coq-exercism-examples

All comments are welcome. It would be interesting to try more complex exercise which will require more tests.

[ErikSchierboom]

Is using modules a standard practice when developing Coq? If so, that seems like a reasonable approach. We should strive to use a setup that is comfortable to Coq users, something they are familiar with.

I've looked at your example code, but the test file is basically just importing another file? Wouldn't it make more sense to just have the basic interface (and its types) defined in the test file? Note that I haven't actually written any Coq, ever :)

I must say I'm quite excited by this potential new track! My thesis used another theorem prover (PVS) to verify software properties.

[vzaliva]

Yes, modules are pretty standard...

In my example, the test is just an import, but in more complex cases after importing it might do some additional checks. I will try to come up with an example. Not sure how do you mean to put an interface in the test file. Now my approach closely mirrors how it is done for OCaml track: module, solution, test (3 files).

Note to self: we need to add timeout as part of unit testing automation. Sometimes proofs take very long time.

[ErikSchierboom]

Maybe that's where my confusion comes from, as most language tracks only use two files:

1. A test file
2. A (stub) implementation file

Consider the accumulate exercise in the Haskell track. When fetching the exercise, the user receives two files:

1. Tests.hs: this file contains the exercise's tests (source)
2. Accumulate.hs: this file is a stub implementation file. The user is provided with a defined function, types and all, but without a valid implementation. (source)

This seems to me a more natural way of organizing things than having 3 files, but maybe it does make sense for Coq.

[vzaliva]

Sure, we can do something like this. I just looked at OCaml so my proposal was inspired by it :)

How do other languages deal with additional types and functions provided? Do they put it in stub implementation file?

[kytrinyx]

It sounds like there's some consensus that this can work, and some ideas for how to make it work.

I'm going to set up the track for you.

• Run bootstrap script
  TRACK_ID=<id> LANGUAGE=<language> bin/bootstrap
• Turn on Travis CI
• Add as a submodule to trackler
  TRACK_ID=<id>; git submodule add https://github.com/exercism/x$TRACK_ID tracks/$TRACK_ID
• Create new team for language
• Add bootstrapped repository to team with write access
• Invite requestor to team

[kytrinyx]

Alrighty, the repo is ready for you.

The launch checklist is here:

http://github.com/exercism/xcoq/issues/1

I'd suggest that you summarize the discussion about how to define the tests that happened above into a new issue in the new repository.

If you find things that are odd or confusing, holler. You can find other track maintainers in the chat room at https://gitter.im/exercism/dev (probably other rooms, too).

Welcome ❤️ ❤️ ❤️

[kytrinyx]

The work to launch this track was never completed, and there has been no activity on the track for a long time.
We are therefore archiving the track repository.

If someone wants to actively build and launch this track, please open an issue in https://forum.exercism.org/c/exercism/building-exercism/125 to discuss it.