Email Gateway (Aug 23 2022 at 09:17): Email Gateway (Aug 23 2022 at 09:17):From: Lawrence Paulson <lp15@cam.ac.uk>
The wiki rosettacode.org collects code snippets in hundreds of programming languages for solving various small tasks, such as Ackermann’s function or tree traversal. There is a wiki page there for Coq: http://rosettacode.org/wiki/Category:Coq
There are also about half a dozen examples. Should we have a presence there, too?
Larry
Email Gateway (Aug 23 2022 at 09:18):From: Manuel Eberl <eberlm@in.tum.de>
Sure!
Email Gateway (Aug 23 2022 at 09:19):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
Sounds like a good idea, yes!
Cheers,
Gerwin
Email Gateway (Aug 23 2022 at 09:20):From: "John F. Hughes" <jfh@cs.brown.edu>
It might be useful to get a consensus on whether what you have is, in fact,
code or not. From
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2019-January/msg00003.html,
we have this:
Email Gateway (Aug 23 2022 at 09:21):From: "C. Diekmann" <diekmann@in.tum.de>
Soooo, it's Friday evening. When and how can I start solving
rosettacode.org tasks
in Isabelle/HOL?
Email Gateway (Aug 23 2022 at 09:21):From: Manuel Eberl <eberlm@in.tum.de>
I don't think they are tasks as such (not in the "Project Euler" sense).
If you feel like doing one in Isabelle, just do it. :)
Manuel
Email Gateway (Aug 23 2022 at 09:21):From: "C. Diekmann" <diekmann@in.tum.de>
Is it just me or does rosettacode not send out email confirmation emails?
Email Gateway (Aug 23 2022 at 09:21):From: "C. Diekmann" <diekmann@in.tum.de>
Okay, finally worked.
I started https://rosettacode.org/wiki/Category:Isabelle.
Email Gateway (Aug 23 2022 at 09:22):From: Makarius <makarius@sketis.net>
I was already aware of that problem when proposing to submit Isabelle document
sources to "rosettacode.org" yesterday on the virtual Isabelle Workshop 2020.
The world out there uses terminology that does not quite fit to what Isabelle
really is, or what it converges to at the limit. But this does not prevent
contact with such external cultures.
The same terminology problem exists with "source code management systems"
(like Mercurial). E.g. see
https://isabelle-dev.sketis.net/source/isabelle/browse/default/src/HOL/Examples/Ackermann.thy
where it is called "source" in the URL and "Code" in the menu button. But the
same happens for README files, where everybody knows that this is not code at all.
Makarius
Email Gateway (Aug 23 2022 at 09:23):From: Lawrence Paulson <lp15@cam.ac.uk>
The examples I was thinking of consisted of purely executable code, no proofs.
Actually there is a case for a similar wiki only for verified code (or other verification examples) undertaken in different proof assistants. We don’t really need to be on the same website as PL/I and SNOBOL.
Larry
Email Gateway (Aug 23 2022 at 09:24):From: "C. Diekmann" <diekmann@in.tum.de>
I don't want to brag, but, ... okay, I'm bragging right now, ..., but I
just implemented https://rosettacode.org/wiki/Brazilian_numbers#Isabelle,
proved the claimed properties stated on rosettacode about Brazilian
numbers, and found that a stated property on rosettacode is actually wrong
<https://rosettacode.org/mw/index.php?title=Brazilian_numbers&diff=prev&oldid=309605>.
Thanks quickcheck and Isabelle/HOL! Proving stuff on a regular coding
website seems to be quite adequate. Also, it's fun :-)
Email Gateway (Aug 23 2022 at 09:25):From: Tobias Nipkow <nipkow@in.tum.de>
Cool! And such a wealth of problems one could apply Isabelle to...
Tobias
smime.p7s
Email Gateway (Aug 23 2022 at 09:26):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
Nice!
Cheers,
Gerwin
Last updated: Apr 27 2024 at 01:05 UTC