3 ms·

I'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 o

by yaseer 8y ago

I'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.

agentultra 8y ago
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!
lamacase 8y ago
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.
brohee 8y ago
Well according to https://deducteam.github.io/ https://deducteam.github.io/ HOL and Coq can be autotranslated to Dedukti (which is the language Logipedia uses)...
seanwilson 8y ago
> Unfortunately, I've never seen enough momentum behind one proof language to give a wiki a chance of becoming something substantial. It's probably not far from hoping for the "Wikipedia of programming" where a single programming is used for all programs. There's religious wars on the best approach to everything and even the proof for "1 + 1 = 2" is fundamentally different in different proof assistants.
HNLurker2 8y ago
Because logic as a subject doesn't have a community in itself and a lot of noise instead of signal (can't find anyone who doesn't mention Gödel against science and maths)

by yaseer 8y ago

agentultra 8y ago

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!

lamacase 8y ago

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.

brohee 8y ago

Well according to https://deducteam.github.io/ https://deducteam.github.io/ HOL and Coq can be autotranslated to Dedukti (which is the language Logipedia uses)...

seanwilson 8y ago

> Unfortunately, I've never seen enough momentum behind one proof language to give a wiki a chance of becoming something substantial. It's probably not far from hoping for the "Wikipedia of programming" where a single programming is used for all programs. There's religious wars on the best approach to everything and even the proof for "1 + 1 = 2" is fundamentally different in different proof assistants.

HNLurker2 8y ago

Because logic as a subject doesn't have a community in itself and a lot of noise instead of signal (can't find anyone who doesn't mention Gödel against science and maths)