Hi, I am a ~50 years old teacher in Computer Science; I have encountered references to Coq for many years without taking the time to investigate more about it yet. I am much into functional programming and curious about learning new languages/systems.
However I have a very specific project in mind and I would like if learning Coq for it would be the best choice.
I am expecting to teach some short initiation-level parts of lambda calculus in about one year, and I would like to use the months to come for writing tools I could use for illustrating various things in lambda calculus.
I am perfectly aware that very good interpreters exist, and I actually compiled some of them, but I enjoy programming and I would like to have my own project anyway.
Currently, I have two different ideas in mind:
- writing my own interpreter (in some language I already know) which would exactly fit my requirements;
- learning Coq and implementing my “examples” and “manipulations” with it.
My requirements are not big: encoding integers in the lambda calculus with several conventions, using the Y combinator, etc. One specific requirement would be to be able to use shortcuts when displaying expressions (“Since we agree to encode the integer 3 in such or such manner, we will display “3” from now on rather than the full lambda expression”, "From now on, I will write “I” rather than “\x.x”, etc.).
I know that Coq is a proof assistant, and I must admit that I am not much concerned (yet?) with the “proof” part; I am rather looking for a tool I could use in front of the student for illustrating basic manipulations. Thus maybe Coq is not the tool I need.
What I am expecting for answers to the current question would be something like:
- really, while doing what you are looking for could (maybe, probably, surely) be achievable, you will not really focus on the most interesting aspects of Coq by using it that way; if you can do what you want by yourself in some other way, you should probably keep Coq for something else later;
- well, main purpose of Coq is not really what you are asking, and some other tools could certainly be some better first choice, but since you said you like learning things, and since Coq can perfectly do it, it would be a great idea trying to do it with Coq!
- doing what you want is very easy with Coq, you should really give it a try!
Thank you by advance,