11–20 of 20 posts
Does it have something like a "test suite" or a "build status" constantly verifying that the various claimed implications and equivalences are valid, and/or that the translations into other languages are valid?
How 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/
Other systems, e.g. Agda use "proof terms" that are more like a proof that can be read "declaratively", but one where every single step has to be recorded; there's no provision for the system to "fill in" some gaps, unlike with declarative proofs. This can definitely impact readability/surveyability of a development, but the inherent maintainance problems of "proof scripts" do not arise.
I'm not sure what Dedukti is going for from this basic POV. They mention that they're trying to build a general framework that can support multiple logical/proof systems, but the details are not that clear. It's probably going to be a bit clunkier than the systems you mention, particularly at this early stage of development.
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…
Something 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 i…
Oh 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.
I've also used it in the design/planning phase of a new project. We started writing models for key features and even hooked TLA+ into our CI pipeline. We planned to also integrate the TLA+ models with quickcheck so that the latter could verify our implementation based on the specification. However that didn't get too far unfortunately.
TLA+ has mostly been useful in helping me understand and solve hard problems where code alone is insufficient as a specification.
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…
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.
How 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/
The systems you mention use a declarative proof approach that's more similar to the way humans might write a math proof, or to the way computer code is written. In contrast, Coq and Lean use "proof scripts" that are more like writing your stuff in a custom macro-assembler that will break as soon as one changes anything in the "script", or even just upgrades to a newer version of the underlying software. Even the resu…
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…