Hello! This community surely has many competitive programmers, right? Where are you? Hint: if 1000000007 and 998244353 look familiar to you, you are a competitive programmer.
I am thinking about making a repository of formalized competitive programming code. I think Coq is a suitable language for this work. I know this is quite open ended, but could you give me advice on how to carry out this project?
A formalized KACTL might be a good idea. Competitive programmers are known for being quite creative. You can give me some other project ideas as well.
I'm actually not that familiar with competitive programming, but do you have in mind the kind of algorithms and theory you typically need for these tasks? I'm assuming it involves some number-theoretical tricks and pointer manipulation at the least, is that right?
It is possible to solve all competitive programming problems without pointers and this is what most people do anyway. Check out https://usaco.guide for the most accurate information on competitive programming.
We do use some NT tricks but nothing advanced. Every high school student knows them.
The most important algorithm that competitive programmers use is brute force. You read that right. Before using more advanced techniques, we often write simple brute force programs to find properties hidden in the problem. These programs are also used to verify the correctness of a more efficient implementation. Of course, if we are strong enough to know the right algorithm for the problem, we implement it right away without brute forcing to explore the problem.
As figuring the algorithm is often much harder than implementing it, I think Coq is helpful for competitive programmers. Coq teaches us mathematical intuition. With Coq, we can prove theorems about the problem that might lead to a full solution.
one general piece of advice is to consider carefully if programs in Coq related to competitive programming are to be executed/evaluated or not [inside Coq as well as outside]. Depending on the libraries that people use, this may be really difficult (e.g., if a function depends on a
well_founded proof that is opaque)
also, it's very likely that competitive programmers will find QuickChick useful
MathComp verified programs are usually represented in such a way as to make proof as easy as possible, and then one uses a refinement library like CoqEAL to make an equivalent program "faster" for evaluation
I used to be active in competitive programming, but I'm brand new to Coq, so I have no advice to give. I think competitive programming problems might make good exercises for formal verification, because they tend to have precise specifications and short but tricky solutions. That said, I hadn't thought of doing it in Coq, since the solutions express themselves most naturally in more C-like languages, but I'm ignorant of Coq's capabilities at that sort of programming.
some formalization problems by the creator of Isabelle is making the rounds, maybe useful for competitive stuff: https://lawrencecpaulson.github.io/2022/08/03/Small-Challenges-I.html
Could I ask one quick question. QuickChick is bundled with Coq Platform, but because it depends on the OCaml compiler, I have to install the Coq Platform from source to use QuickChick right?
And after installing the Coq Platform from source, I could use QuickChick immediately. Is that correct.
I tried out a QuickChick command without installing anything except the Coq Platform. And the command was recognized, but I got an error saying that ocamlbuild was not found.
Yes it must be from source, and if it doesn't work immediately after that you can complain here on Zulip or here https://github.com/QuickChick/QuickChick/issues/269
https://github.com › mit-plv › fiat-cr...
mit-plv/fiat-crypto: Cryptographic Primitive Code Generation by Fiat - GitHub
Wtf am I seeing
Ik little to nothing as to how to code yet I can only know when things are off. Someone help
@G Host we can’t tell what is the problem
Last updated: Sep 26 2023 at 12:02 UTC