Email Gateway (Aug 22 2022 at 19:56): Email Gateway (Aug 22 2022 at 19:56):From: Makarius <makarius@sketis.net>
No, just the common sense you apply in the virtual village of a
scientific community. In principle everybody knows each other, directly
or indirectly via 1-2 intermediates, and you could eventually meet up in
person on a workshop or conference. Of course, there is no obligation to
start as a well-known insider, but there needs to be some openness to
become one eventually.
Contributors to Isabelle and/or AFP need to be trustworthy and
personally accountable for what they do. The LCF approach does not
protect against non-sense that can be done on a shared repository. (I am
not going to explain further details how and what could be done there.)
Makarius
Email Gateway (Aug 22 2022 at 19:56):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
The problem in the case of Wikipedia is that anonymous contributors can
contribute rubbish without being held accountable for it under their
real identities. However, in the case of the AFP we have a review
process (this is at least what I thought); so rubbish contributions
should never make it into the AFP, independently of whether they are
contributed anonymously or not.
All the best,
Wolfgang
Email Gateway (Aug 22 2022 at 19:56):From: Makarius <makarius@sketis.net>
The rubbish production on Wikipedia works quite differently -- by people
who are proven experts (sometimes backed by big corporations or other
interest groups). Likewise, and still quite different, is the abuse by
some people on Stackoverflow with a lot of points. Neither of these
systems work according to their official description on the front-page.
Compared to that our Isabelle/AFP global village and virtual garden is
really great.
Makarius
Email Gateway (Aug 22 2022 at 19:57):From: Makarius <makarius@sketis.net>
You are right that there is a danger to diverge into questions of policy
that are alien to this mailing list. So in a narrow sense that is off-topic.
In a broader sense it is on topic: Isabelle/AFP is getting more and more
important and it could become something like a formal Wikipedia or
Stackoverflow eventually. Some colleagues have occasionally started to
think about proper research projects in such a direction.
So in the near future, questions of policies, ethics, the general social
model etc. in our public libraries of formalized mathematics might
become very relevant. Pure Logic and Mathematics are not free from
impact to the real (and messy) world.
Makarius
Email Gateway (Aug 22 2022 at 20:05):From: Lawrence Paulson <lp15@cam.ac.uk>
I didn’t quite understand what you’ve done here, but its potential sounds tremendous. I’d like know more about this. For example, are you able to derive some of the theorems in Analysis/Abstract_Topology from their type class analogues without needing separate proofs?
Larry Paulson
Email Gateway (Aug 22 2022 at 20:05):From: Fabian Immler <immler@in.tum.de>
Thank you for sharing this, this is a very useful development and at a
first glance, the code looks (at least to me) reasonably Isabelle/ML
idiomatic!
To keep the expectations (that non-Types-To-Sets experts might have)
realistic: The framework hides the "local typedef" part of the
Types-To-Sets approach nicely. But I don't think this can already be
seen as a tool that enables an end-user to casually relativize theorems.
This is because one needs to know a lot about the hierarchical structure
(i.e, one needs to provide a set-based locale hierarchy along the
hierarchy of type-classes in HOL and manually establish appropriate
relationships between them) of the underlying type-based formalization
as well as the theoretical and technical (especially the transfer
method) background.
That said, it is extremely helpful for a systematic relativization of
existing libraries (as you have demonstrated with your numerous
applications). And those relativized libraries can then be used easily
by non-experts.
I'd be glad to see a formalization of e.g.,
HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy based on your framework.
I like your tts_statistics command (although I don't understand what the
argument "cc" should stand for), it seems like this could be used as a
means to keep relativized libraries in sync with the underlying
non-relativized developments. One could imagine that a relativizing
session fails to build when not all theorems of the underlying
type-based library are relativized.
I believe your developments (and also the applications) should be
incorporated into the isabelle repository, and better sooner than later.
This is in order to avoid bit-rot and to ease improvements and
contributions by other developers. I'd be happy to help (from an
engineering point of view) incorporating this in the development version
of Isabelle, but I am not so sure how to deal with the legal issues (if
there are any) of contributions that are published by an anonymous
contributor under a different license.
Best regards,
Fabian
smime.p7s
Email Gateway (Aug 22 2022 at 20:05):From: Fabian Immler <immler@in.tum.de>
I guess I can add this: I'm neither maintaining Isabelle nor the AFP,
but I believe you must disclose your identity in order to have your
developments accepted in the Isabelle repository or in the AFP.
If it is not in one of those places, nobody will use or maintain your
developments and that would be a shame.
Fabian
smime.p7s
Email Gateway (Aug 22 2022 at 20:06):From: Lars Hupel <hupel@in.tum.de>
Looking at the history of Isabelle+AFP, there are many contributions
where the authors have moved on from academia and/or Isabelle. I see no
observable difference between that case and pseudonymous contributions.
Cheers
Lars
Email Gateway (Aug 22 2022 at 20:06):From: Makarius <makarius@sketis.net>
By definition everything in the Isabelle repository is subject to its
BSD-style license in the toplevel directory: all named contributors have
explicitly or implicitly agreed to that in a legally binding way. (An
anonymous dummy is not a legal entity.)
The Isabelle application bundle is different: it agglomerates multiple
projects with multiple licenses like a Linux distribution.
Makarius
Email Gateway (Aug 22 2022 at 20:06):From: Makarius <makarius@sketis.net>
Contributors that cannot be publicly identified have done great harm to
projects like Wikipedia: a lot of its content is now rubbish, especially
on topics of economic or political interest. Hopefully our great Archive
of Formal Proofs is not moving in such a direction.
Makarius
Email Gateway (Aug 22 2022 at 20:07):From: Lars Hupel <hupel@in.tum.de>
Are you suggesting introducing a government ID check for submissions?
Because we don't do that presently. If our anonymous poster would've
gone with a name akin to "Jane Doe", we wouldn't even have this
conversation.
Last updated: Apr 26 2024 at 08:19 UTC