Logipedia – Encyclopedia of Formal Proofs
logipedia.inria.fr
Logipedia – Encyclopedia of Formal Proofs
1–10 of 20 posts
Re: Logipedia – Encyclopedia of Formal Proofs
#2Oh very good!
I started a repository for TLA+ modules years ago that I was hoping would turn into something like this [0]. Like many projects I never took it very far but I've been using formal methods in practice for a couple of years now, might be worth revisiting...
Re: Logipedia – Encyclopedia of Formal Proofs
#3I've always wanted a 'Wikipedia for formal proofs'. It's never materialised though, sadly.
I would've expected such an online Encyclopedia to form around Coq or Isabelle/HOL, as these languages/assistants seem to be the most popular.
Unfortunately, I've never seen enough momentum behind one proof language to give a wiki a chance of becoming something substantial.
It seems the formal proof community (which is already small) is so spread out over several languages, that it's hard to get the fire burning.
Re: Logipedia – Encyclopedia of Formal Proofs
#4I've always wanted a 'Wikipedia for formal proofs'. It's never materialised though, sadly. I would've expected such an online Encyclopedia to form around Coq or Isabelle/HOL, as these languages/assistants seem to be the most popular. Unfortunately, I've never seen enough momentum behind one proof language to give a wiki a chance of becoming something substantial. It seems the formal proof community (which is already…
I think a large part of it may be that people are still inventing the languages and we haven't seen enough industry adoption to settle down on a handful of good ones.
We're still in the Cambrian explosion of new ideas and languages.
The best way to get to the future you want is to keep using them and convincing others to join you!
Re: Logipedia – Encyclopedia of Formal Proofs
#5How does this relate to the Archive of Formal Proofs [1] and Mizar's Mathematical Library [2]?
Re: Logipedia – Encyclopedia of Formal Proofs
#6Something related to this Logipedia that I'd be interested to see (or work on building one day) is a site intermediate between this and Wikipedia -- a site where users can view or create logical arguments, and combine smaller arguments into larger ones. I'm not sure how many people would actually use such a site, but it'd surely promote a higher level of public discourse than, say, Twitter. The only way we really communicate online is using strings; there has to be some potential for something more structured.
Re: Logipedia – Encyclopedia of Formal Proofs
#7I've always wanted a 'Wikipedia for formal proofs'. It's never materialised though, sadly. I would've expected such an online Encyclopedia to form around Coq or Isabelle/HOL, as these languages/assistants seem to be the most popular. Unfortunately, I've never seen enough momentum behind one proof language to give a wiki a chance of becoming something substantial. It seems the formal proof community (which is already…
How about a "Rosetta Proof" wiki in the style of "Rosetta Code"? You wouldn't need to settle on one language, and it might help clarify the advantages of one language or another.
Re: Logipedia – Encyclopedia of Formal Proofs
#8How does this relate to the Archive of Formal Proofs [1] and Mizar's Mathematical Library [2]? [1] https://www.isa-afp.org/ [2] http://mizar.org/library/
You can also add Coq's to the mix:
[3] https://coq.inria.fr/library/
Each 1-3 is language specific (Isabelle/HOL, Mizar and Coq respectively).
Logipedia too, is using the language Dedukti, although it is designed to translate into other proof languages, and list these on Logipedia.
Re: Logipedia – Encyclopedia of Formal Proofs
#9Something related to this Logipedia that I'd be interested to see (or work on building one day) is a site intermediate between this and Wikipedia -- a site where users can view or create logical arguments, and combine smaller arguments into larger ones. I'm not sure how many people would actually use such a site, but it'd surely promote a higher level of public discourse than, say, Twitter. The only way we really com…
I feel like we need a wiki/wolfram-esque system where knowledge is derived from axioms, propositions, and theorems, all of which can be toggled and shared by users. If you have the flat-earth axiom toggled on, or some set of axioms and propositions that lead to a flat-earth theorem, then you'll see a different entry of knowledge about the earth than I will. We just have to accept that nothing is completely provable in any concrete sense, and people will disagree about the noumenon. Flat-earth is an extreme example, but there are ambiguous parts of our models that you can interpret different ways, and data that can be reasonably argued as (in)valid. I think a unified system of disunity would be more clever than the patchwork of IdeologyPedias we have today. Once sets of truths have been distributed they could be given precedence by a user, with additional optional toggling, and then used/redistributed. I remember seeing an open-source project attempting this, I thought it was called OneModel but my google searches for that name are turning up an unrelated data company. The code seemed pretty gnarly to me at the time, but it's been a couple years since I looked at it.
Edit: changed ridiculous grammar for clarity.
Re: Logipedia – Encyclopedia of Formal Proofs
#10Oh very good! I started a repository for TLA+ modules years ago that I was hoping would turn into something like this [0]. Like many projects I never took it very far but I've been using formal methods in practice for a couple of years now, might be worth revisiting... [0] https://github.com/agentultra/software-spec-library
what kinds of ways have you been applying TLA? I've been considering whether it's worth learning for practical purposes.