5 ms·

> Most verification systems work in terms of hours or days. What kind of verification does usually take hours? Just checked how long it takes to verify Raft us

by h91wka 7y ago

> Most verification systems work in terms of hours or days. What kind of verification does usually take hours? Just checked how long it takes to verify Raft using Coq and Verdi (pretty sizeable proof), and complete pipeline takes around 25 minutes (with Docker container creation, fetching dependencies, and what not). Verification of proof terms is a relatively easy task for a computer, as easy as type checking. Coming up with the proofs, on the other hand, that is hard.

digama0 7y ago
The verification of entire proof libraries (like the entire Coq standard library, or the Isabelle Archive of Formal proofs) usually ranges from hours to days, as do some of the larger computer science projects like seL4 and CakeML. You are right, verification is much faster than coming up with proofs, and that explains the majority of the disparity. But then why are we reinventing proofs so much? This is clearly needless work, and there are a thousand ways to solve the problem but even recognizing that it is a problem is difficult in certain circles.
dwheeler 7y ago
The 25 minute value is only the time to verify a single Coq proof. I'm measuring the time to verify ALL proofs of an entire system. The Metamath Rust verifier normally verifies 23,000+ proofs at a time. The actual verification time is just less than 1 second for the entire set. When you include the time for container creation, fetching dependencies, and so on, it typically takes ~48 seconds for it to verify the entirety of set.mm (which includes thousands of proofs). Here's an example: https://travis-ci.org/metamath/set.mm/builds/602369640 https://travis-ci.org/metamath/set.mm/builds/602369640 You could run 23,000 Coq jobs in parallel. I wouldn't want to pay for it :-). And it would complete verification of all the proofs in 25 minutes, vs. the 200msec of Metamath Zero or the ~1 second of the Metamath Rust implementation. That's not to say that Coq is a terrible system. Coq is really interesting! But verification time is not something it's prioritized.
- h91wka 7y ago
  > The 25 minute value is only the time to verify a single Coq proof. Logically it is a singe proof, but technically it consists of quite a few theorems and lemmas, so this is not a valid comparison. Also proofs in Coq are typically structured and pretty high-level because of all the automation, while metamath proofs look like core dumps :) ${ $d A a b v w x y $. $d B a b v w x y $. $d F a b v w x y $. $( The ` 2nd ` (second member of an ordered pair) function restricted to a one-to-one function ` F ` is a one-to-one function of ` F ` onto the range of ` F ` . (Contributed by Alexander van der Vekens, 4-Feb-2018.) $) f1o2ndf1 $p |- ( F : A -1-1-> B -> ( 2nd |` F ) : F -1-1-onto-> ran F ) $= ( vx vy va vv vb vw c2nd syl cv cfv wceq wi wcel wa wrex ex com23 wf1 crn cres wfo ccnv wfun wf1o f1f fo2ndf weq wral f2ndf cxp wss fssxp cop ssel2 elxp2 sylib anim12dan fvres adantr ad2antlr eqeq12d op2nd eqeq12i funopfv wf vex f1fun anim12d eqcom biimpi eqeqan12d simpl anim12i f1veqaeq sylan2 opeq12 syl6 com14 syl6bi pm2.43i syld impcom syl5bi sylbid adantl adantlr com13 com12 wb eleq1 bi2anan9 anbi2d fveq2 simpllr imbi12d imbi2d 3imtr4d simpr rexlimdvva rexlimivv imp mpcom ralrimivv dff13 df-f1 simprbi dff1o3 sylanbrc ) ABCUAZCCUBZJCUCZUDZXNUEUFZCXMXNUGXLABCVHZXOABCUHZABCUIKXLCBXNU AZXPXLCBXNVHZDLZXNMZELZXNMZNZDEUJZOZECUKDCUKXSXLXQXTXRABCULKXLYGDECCCABUM ZUNZXLYACPZYCCPZQZYGOXLXQYIXRABCUOKYIYLXLYGYIYLXLYGOZYAFLZGLZUPZNZGBRFARZ YCHLZILZUPZNZIBRHARZQYIYLQZYMYIYJYRYKUUCYIYJQYAYHPYRCYHYAUQFGYAABURUSYIYK QYCYHPUUCCYHYCUQHIYCABURUSUTYRUUCUUDYMOZYQUUCUUEOZFGABYNAPZYOBPZQZYQUUFUU IYQQZUUBUUEHIABUUJYSAPZYTBPZQZQZUUBUUEUUNUUBQZYIYPCPZUUACPZQZQZXLYPXNMZUU AXNMZNZYPUUANZOZOZUUDYMUUNUUSUVEOZUUBUUIUUMUVFYQUUSUUIUUMQZUVEUURUVGUVEOY IUURUVGUVEUURUVGQZUVBXLUVCUVHUVBYPJMZUUAJMZNZXLUVCOZUVHUUTUVIUVAUVJUURUUT UVINZUVGUUPUVMUUQYPCJVAVBVBUUQUVAUVJNUUPUVGUUACJVAVCVDUVKGIUJZUVHUVLUVIYO UVJYTYNYOFVIGVIVEYSYTHVIIVIVEVFUVHXLUVNUVCUVGUURXLUVNUVCOZOXLUURUVGUVOXLU URYNCMZYONZYSCMZYTNZQZUVGUVOOXLCUFZUURUVTOABCVJUWAUUPUVQUUQUVSYNYOCVGYSYT CVGVKKXLUVGUVTUVOUVNUVGUVTXLUVCUVNUVGUVTUVLOOUVTUVNUVGUVNUVLUVTUVNUVPUVRN ZUVGUVNUVLOOUVQUVSYOUVPYTUVRUVQYOUVPNUVPYOVLVMUVSYTUVRNUVRYTVLVMVNXLUVGUV NUWBUVCXLUVGUVNUWBUVCOOXLUVGQZUWBUVNUVCUWCUWBFHUJZUVOUVGXLUUGUUKQUWBUWDOU UIUUGUUMUUKUUGUUHVOUUKUULVOVPABYNYSCVQVRUWDUVNUVCYNYOYSYTVSSVTTSWAWBWAWCW ATWDWJWETWFWGTSWHWKWIVBUUOYLUURYIUUNYJUUPUUBYKUUQYQYJUUPWLUUIUUMYAYPCWMVC YCUUACWMWNWOUUOYGUVDXLUUOYEUVBYFUVCUUNUUBYBUUTYDUVAYQYBUUTNUUIUUMYAYPXNWP VCYCUUAXNWPVNUUOYAYPYCUUAUUIYQUUMUUBWQUUNUUBXAVDWRWSWTSXBSXCXDXESTXEXFDEC BXNXGXKXSXTXPCBXNXHXIKCXMXNXJXK $. $} ...
lidHanteyk 7y ago
I encourage you to try Metamath. When starting a new axiom system from scratch, I found that I was not capable of writing anything that would cause lag; I wasn't able to make Metamath the slow part of my workflow. No matter how I approached it, the slowest parts of my work were my typing (with my fingers) and my typing (with my mind and whiteboard). No other formal proof assistant has been this fast for me. The next closest one is Idris, which is type-theory-driven (fancy phrase for "slow") and it takes a few moments to round-trip between the REPL and the text editor.
- h91wka 7y ago
  > the slowest parts of my work were my typing My rule of thumb says: if fingers are the bottleneck, then your programming language is not powerful enough (too verbose). Working with higher level abstractions is good for health: brain doesn't get RSI. > which is type-theory-driven (fancy phrase for "slow") ...
  - digama0 7y ago
    What if your brain is the bottleneck?
  - lidHanteyk 7y ago
    Syntax-only formalisms are faster than semantically-laden formalisms; a compiler's parser is usually faster than its backend. Metamath is going to always be faster than Coq, Lean, Isabelle, HOL, Agda, Idris, or indeed much weaker systems like Haskell. There's no RSI in working with Metamath. What I mean is that the workflow is largely dependent on me knowing what I want to prove and roughly how I want to prove it, rather than Metamath chewing CPU.

by h91wka 7y ago

digama0 7y ago

The verification of entire proof libraries (like the entire Coq standard library, or the Isabelle Archive of Formal proofs) usually ranges from hours to days, as do some of the larger computer science projects like seL4 and CakeML. You are right, verification is much faster than coming up with proofs, and that explains the majority of the disparity. But then why are we reinventing proofs so much? This is clearly needless work, and there are a thousand ways to solve the problem but even recognizing that it is a problem is difficult in certain circles.

dwheeler 7y ago

The 25 minute value is only the time to verify a single Coq proof. I'm measuring the time to verify ALL proofs of an entire system. The Metamath Rust verifier normally verifies 23,000+ proofs at a time. The actual verification time is just less than 1 second for the entire set. When you include the time for container creation, fetching dependencies, and so on, it typically takes ~48 seconds for it to verify the entirety of set.mm (which includes thousands of proofs). Here's an example: https://travis-ci.org/metamath/set.mm/builds/602369640 https://travis-ci.org/metamath/set.mm/builds/602369640 You could run 23,000 Coq jobs in parallel. I wouldn't want to pay for it :-). And it would complete verification of all the proofs in 25 minutes, vs. the 200msec of Metamath Zero or the ~1 second of the Metamath Rust implementation. That's not to say that Coq is a terrible system. Coq is really interesting! But verification time is not something it's prioritized.

h91wka 7y ago
> The 25 minute value is only the time to verify a single Coq proof. Logically it is a singe proof, but technically it consists of quite a few theorems and lemmas, so this is not a valid comparison. Also proofs in Coq are typically structured and pretty high-level because of all the automation, while metamath proofs look like core dumps :) ${ $d A a b v w x y $. $d B a b v w x y $. $d F a b v w x y $. $( The ` 2nd ` (second member of an ordered pair) function restricted to a one-to-one function ` F ` is a one-to-one function of ` F ` onto the range of ` F ` . (Contributed by Alexander van der Vekens, 4-Feb-2018.) $) f1o2ndf1 $p |- ( F : A -1-1-> B -> ( 2nd |` F ) : F -1-1-onto-> ran F ) $= ( vx vy va vv vb vw c2nd syl cv cfv wceq wi wcel wa wrex ex com23 wf1 crn cres wfo ccnv wfun wf1o f1f fo2ndf weq wral f2ndf cxp wss fssxp cop ssel2 elxp2 sylib anim12dan fvres adantr ad2antlr eqeq12d op2nd eqeq12i funopfv wf vex f1fun anim12d eqcom biimpi eqeqan12d simpl anim12i f1veqaeq sylan2 opeq12 syl6 com14 syl6bi pm2.43i syld impcom syl5bi sylbid adantl adantlr com13 com12 wb eleq1 bi2anan9 anbi2d fveq2 simpllr imbi12d imbi2d 3imtr4d simpr rexlimdvva rexlimivv imp mpcom ralrimivv dff13 df-f1 simprbi dff1o3 sylanbrc ) ABCUAZCCUBZJCUCZUDZXNUEUFZCXMXNUGXLABCVHZXOABCUHZABCUIKXLCBXNU AZXPXLCBXNVHZDLZXNMZELZXNMZNZDEUJZOZECUKDCUKXSXLXQXTXRABCULKXLYGDECCCABUM ZUNZXLYACPZYCCPZQZYGOXLXQYIXRABCUOKYIYLXLYGYIYLXLYGOZYAFLZGLZUPZNZGBRFARZ YCHLZILZUPZNZIBRHARZQYIYLQZYMYIYJYRYKUUCYIYJQYAYHPYRCYHYAUQFGYAABURUSYIYK QYCYHPUUCCYHYCUQHIYCABURUSUTYRUUCUUDYMOZYQUUCUUEOZFGABYNAPZYOBPZQZYQUUFUU IYQQZUUBUUEHIABUUJYSAPZYTBPZQZQZUUBUUEUUNUUBQZYIYPCPZUUACPZQZQZXLYPXNMZUU AXNMZNZYPUUANZOZOZUUDYMUUNUUSUVEOZUUBUUIUUMUVFYQUUSUUIUUMQZUVEUURUVGUVEOY IUURUVGUVEUURUVGQZUVBXLUVCUVHUVBYPJMZUUAJMZNZXLUVCOZUVHUUTUVIUVAUVJUURUUT UVINZUVGUUPUVMUUQYPCJVAVBVBUUQUVAUVJNUUPUVGUUACJVAVCVDUVKGIUJZUVHUVLUVIYO UVJYTYNYOFVIGVIVEYSYTHVIIVIVEVFUVHXLUVNUVCUVGUURXLUVNUVCOZOXLUURUVGUVOXLU URYNCMZYONZYSCMZYTNZQZUVGUVOOXLCUFZUURUVTOABCVJUWAUUPUVQUUQUVSYNYOCVGYSYT CVGVKKXLUVGUVTUVOUVNUVGUVTXLUVCUVNUVGUVTUVLOOUVTUVNUVGUVNUVLUVTUVNUVPUVRN ZUVGUVNUVLOOUVQUVSYOUVPYTUVRUVQYOUVPNUVPYOVLVMUVSYTUVRNUVRYTVLVMVNXLUVGUV NUWBUVCXLUVGUVNUWBUVCOOXLUVGQZUWBUVNUVCUWCUWBFHUJZUVOUVGXLUUGUUKQUWBUWDOU UIUUGUUMUUKUUGUUHVOUUKUULVOVPABYNYSCVQVRUWDUVNUVCYNYOYSYTVSSVTTSWAWBWAWCW ATWDWJWETWFWGTSWHWKWIVBUUOYLUURYIUUNYJUUPUUBYKUUQYQYJUUPWLUUIUUMYAYPCWMVC YCUUACWMWNWOUUOYGUVDXLUUOYEUVBYFUVCUUNUUBYBUUTYDUVAYQYBUUTNUUIUUMYAYPXNWP VCYCUUAXNWPVNUUOYAYPYCUUAUUIYQUUMUUBWQUUNUUBXAVDWRWSWTSXBSXCXDXESTXEXFDEC BXNXGXKXSXTXPCBXNXHXIKCXMXNXJXK $. $} ...

lidHanteyk 7y ago

I encourage you to try Metamath. When starting a new axiom system from scratch, I found that I was not capable of writing anything that would cause lag; I wasn't able to make Metamath the slow part of my workflow. No matter how I approached it, the slowest parts of my work were my typing (with my fingers) and my typing (with my mind and whiteboard). No other formal proof assistant has been this fast for me. The next closest one is Idris, which is type-theory-driven (fancy phrase for "slow") and it takes a few moments to round-trip between the REPL and the text editor.

h91wka 7y ago
> the slowest parts of my work were my typing My rule of thumb says: if fingers are the bottleneck, then your programming language is not powerful enough (too verbose). Working with higher level abstractions is good for health: brain doesn't get RSI. > which is type-theory-driven (fancy phrase for "slow") ...
- digama0 7y ago
  What if your brain is the bottleneck?
- lidHanteyk 7y ago
  Syntax-only formalisms are faster than semantically-laden formalisms; a compiler's parser is usually faster than its backend. Metamath is going to always be faster than Coq, Lean, Isabelle, HOL, Agda, Idris, or indeed much weaker systems like Haskell. There's no RSI in working with Metamath. What I mean is that the workflow is largely dependent on me knowing what I want to prove and roughly how I want to prove it, rather than Metamath chewing CPU.