Email Gateway (Aug 22 2022 at 18:43): Email Gateway (Aug 22 2022 at 18:43):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
A practical way to prevent cheating is to ask to the participants to upload
a video of they solving the problem to youtube or a similar website (videos
uploaded 1/2 hour after the end of the competition will be ignored). Only
the videos of the winners will be checked by humans, increasing the speed
of the films. For people with less economic resources, this option is
better than to travel to another continent in order to participate in a
contest. This is just theory, in case someday something similar will be
implemented.
Kind Regards,
José M.
Email Gateway (Aug 22 2022 at 18:44):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear All,
Thank you for your replies with regard to my comment about proving contests
and please accept my apologies for resurrecting an old topic. I have to
admit that my comment was written in awkward circumstances and,
unfortunately, did not convey its intended meaning. Moreover, the comment
may have sounded slightly aggressive, which also was not my intention.
Unfortunately, in this comment, I failed to mention that, of course, I
completely support all proposals and existing contests in the areas of
formal proof and formal verification.
I would also like to emphasize that my comment was made in relation to the
proposal of organizing the "Internation Olympiad in Isabelle" (or,
alternatively, "Internation Olympiad in Formal Proof and Verification")
that was made by José Manuel Rodriguez Caballero and not in relation to any
other contest (i.e. a contest that bears a name that does not start with
the phrase "Internation Olympiad in..."). To the best of my knowledge, all
international olympiads (i.e. all contests that bear names that start with
the phrase "International Olympiad in...") require the presence of
participants on site and take many other steps to prevent cheating.
Moreover, it is likely to be very uncommon for participants to pay for
their travel expenses to international olympiads because they are usually
sponsored by their governments (even participants from less developed
countries). However, of course, admission committees at universities and
employers treat international olympiads much more seriously than all other
events.
Thank you
A practical way to prevent cheating is to ask to the participants to upload
a video of they solving the problem to youtube or a similar website (videos
uploaded 1/2 hour after the end of the competition will be ignored). Only
the videos of the winners will be checked by humans, increasing the speed
of the films. For people with less economic resources, this option is
better than to travel to another continent in order to participate in a
contest. This is just theory, in case someday something similar will be
implemented.
Kind Regards,
José M.
Dear all,
for our system, we foresee to also get other theorem provers on board.
For each theorem prover, one needs to find a volunteer who is willing to
implement a prover backend,
and who is willing to formulate the tasks for the theorem prover.As for most programming competitions, our main goal is to spark
motivation. For this purpose, in my opinion, the
only way is to host the competition online, as only then everyone has the
possibility to participate.I agree that if you want to hand out an important prize, you will always
need to make sure that
the person you give the prize to will be the one who actually solved the
problems. However,
I believe this is already ten steps ahead of where we stand now.
Dear All,
I would like to make several comments with regard to the proposal by José
Manuel Rodriguez Caballero (as someone who participated in olympiads while
studying at secondary school).
Of course, the olympiads in informatics can hardly be described as
olympiads that test the participants on their knowledge of the syntax of a
particular programming language. The main challenge is the design of
algorithms and not their implementation. The participants are allowed to
select a programming language. While the choice is relatively narrow (C++,
Pascal and Java), they seem to be working on expanding this choice (until
recently the participants were allowed to use only C, C++ and Pascal).
While Isabelle is one of the most popular proof assistants, it is not the
only available proof assistant. I believe that Coq is equivalently popular
and has nearly identical functionality (for example, there are more
questions about Coq on Stack Overflow than about Isabelle). Of course,
there are other well-known systems for proof verification.
Personally, I prefer Isabelle and I would like to see it succeed. However,
if one was to organise an international olympiad that allows its
participants to use Isabelle, in my opinion, it would need to be an
olympiad in the proof verification/logic/formal methods and not an olympiad
"in Isabelle". From the start, it should allow the participants to use
either Isabelle or Coq. Also, of course, the tasks should reflect that the
participants are being tested on their knowledge of the methods that are
commonly used for the formalisation of mathematics or formal proof of
computer programs and not the knowledge of the 'advanced features' of a
given proof assistant. Thus, the organisers would have to carefully select
the subsets of the standard libraries that one is allowed to use during the
olympiad.
Also, personally, in my view, participation over the internet should not
be allowed, because it favours cheating. Being able to claim that one has a
prize in an olympiad in formal verification would provide an enormous
competitive advantage when one is applying to universities (and beyond).
Thus, cheating must be eliminated at all costs. It may be best (for the
sake of humanity) not to organise such an olympiad at all, rather than
allowing the participation over the internet. Also, of course, there should
be different olympiads for secondary school students and undergraduate
students.
Thank you
Email Gateway (Aug 22 2022 at 18:44):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
mailing-list anonymous wrote:
I have to admit that my comment [concerning cheating in an olympiad by
internet] was written in awkward circumstances and,
unfortunately, did not convey its intended meaning. Moreover, the comment
may have sounded slightly aggressive, which also was not my intention.
There is not aggressiveness in pointing out that there are people who cheat
in life: this is the reason why cryptography and security engineering
exist. In one phrase due to the great MILAN KUNDERA: Only animals were not
expelled from Paradise. https://en.wikipedia.org/wiki/Milan_Kundera
mailing-list anonymous wrote:
Moreover, it is likely to be very uncommon for participants to pay for
their travel expenses to international olympiads because they are usually
sponsored by their governments (even participants from less developed
countries)
You already mentioned the possibility of individual people cheating. Well,
there is the possibility of some governments cheating too. I have many
friends who will start laughing if someone talks about the honesty of their
governments. I do not want to talk about politics. So, I leave it to your
imagination.
Kind Regards,
José M.
Last updated: May 06 2024 at 20:16 UTC