Top 14 coq Open-Source Projects
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.Project mention: Which Prof for 191? | reddit.com/r/UBreddit | 2021-10-06
The CompCert formally-verified C compilerProject mention: Multicore OCaml: September 2021, effect handlers will be in OCaml 5.0 | news.ycombinator.com | 2021-10-04
OCaml is becoming a must learn language for those who want to take their C programming to the highest levels, because:
1. Frama-C, which enables writing bug-free C programs, is implemented using a combination of OCaml and the Coq proof assistant (which is itself implemented in OCaml):
2. CompCert, a formally verified C compiler, is implemented using OCaml and Coq:
Nothing at this level yet exists in the Rust and Zig ecosystems, for example. Rust is a very complicated language with many features which makes formalization much harder than with C and OCaml, which both had mathematical ideas of simplicity, analyzability, and minimalism inspire their designs, even if they continue to grow into more complicated monsters, which, incidentally this OCaml 5.0 release will contribute towards. :-)
Scout APM: A developer's best friend. Try free for 14-days. Scout APM uses tracing logic that ties bottlenecks to source code so you know the exact line of code causing performance issues and can get back to building a great product faster.
I have found some instances of jsCoq but nothing else. Do you know some other online platform? (Whatever the underlying prover or logic)
A gently curated list of companies using verification formal methods in industryProject mention: A list of companies that use formal verification methods | news.ycombinator.com | 2021-02-08
A function definition package for CoqProject mention: Learn coq or agda before diving into idris2? | reddit.com/r/dependent_types | 2021-05-02
I'd say Agda is more similar to Idris than Coq. Coq has a different syntax and isn't as good for programming with dependent types as Agda and Idris (Agda and Idris both put a huge emphasis on dependent pattern matching, something that Coq only recently gained support for through the Equations package).
Interactive Coq Proofs in VimProject mention: Is MATH145 worth it? | reddit.com/r/uwaterloo | 2021-09-15
If you're finding coqide hard to use, I used to use coquille back in the day so that I didn't have to lose my neovim workflow (though it seems like coqtail is the currently maintained fork). I remember djao himself used to use proof general with emacs, which looks like another nice option if you're an emacs user.
Coq Protocol Playground with Se(xp)rialization of Internal Structures.Project mention: Translating My Z3 Tutorial to Coq | news.ycombinator.com | 2021-02-27
It's a question I hadn't really considered before. On first pass, as far as I know, I'd say the answer is no. It isn't clear to me what the objective of embedding Coq with a C api for example would be. The very core of Coq is about verifying proofs and not producing them and I'm not sure what the benefit of embedding it is.
Having said that there are a few projects that may be something like what you're asking. First off, Coq has the SerAPI project https://github.com/ejgallego/coq-serapi through which external programs can talk to coq. This has been used for example to make a python OpenAi gym like interface https://github.com/princeton-vl/CoqGym.
A different direction might be something like MetaMath Zero https://arxiv.org/abs/1910.10703 which is intended to be a small and fast verifier for it's language, perhaps maybe someday for embedding in applications. There is this notion of "Proof Carrying Code" which I don't really know what the current state of the art is. https://en.wikipedia.org/wiki/Proof-carrying_code One might want an easily embeddable trusted verifier for that purpose. I don't know.
Run Linux Software Faster and Safer than Linux with Unikernels.
Project mention: The Fundamental Theorem of Algebra in ACL2 | news.ycombinator.com | 2021-07-29
> Or there are these high level systems for proving deep theorems. Is anyone trying to fill the gap?
There's ongoing work on computable real numbers for instance the CoRN library, so hope is on the horizon, for instance, a recent update to the Coq Interval package adds certified plotting, that is, the library guarantees that if a function passes through a pixel, that pixel is filled. There's also the user-friendly Coquelicot real analysis library up to basic differential equations (e.g. Bessel function).
> It'll rearrange an equation but I can't ask it "prove this is increasing"
For a taste, here's my proof that the cube function is increasing. If I wanted to create a tactic that automatically proves a function is increasing, I would use properties of increasing functions to recursively break it down into trivial subcases.
Formal proof of the Four Color TheoremProject mention: Solution to the four color theorem in haskell | reddit.com/r/haskell | 2021-05-27
A minimalistic blockchain consensus implemented and verified in CoqProject mention: A minimalistic blockchain consensus implemented and verified in Coq | news.ycombinator.com | 2021-03-04
Formal specification and verification of hardware, especially for security and privacy.Project mention: Silveroak - Formal specification and verification of hardware | reddit.com/r/Coq | 2021-05-20
PhD research ;; What's the difference between a typeclass/trait and a record/class/struct? Nothing really, or so I argue.Project mention: The Next 700 Module Systems [pdf] | news.ycombinator.com | 2021-05-23
A library of mechanised undecidability proofs in the Coq proof assistant.Project mention: Math proof databases | reddit.com/r/mathematics | 2021-04-14
There are two problems. The first is that there is no central repository. Sure, maybe if you're interested in undecidable results you might go here... But it's an island, and so is every other library. Worse yet, there's little inter mixing or combinable ways to use libraries. Unlike other programming languages, automated proof systems have so far been aimed at the technical aspects of a single person proving something, rather than the shareability of proofs.
COQ.nvim support for WordPress hooksProject mention: popui.nvim - GUI popfix per codeAction (e forse anche altro) | reddit.com/r/ItalyInformatica | 2021-10-10
PS: io ho solo fatto un plugin per Coq https://github.com/Mte90/coq_wordpress e i meiie dotfiles https://github.com/mte90/dotfiles
What are some of the best open-source coq projects? This list will help you:
Are you hiring? Post a new remote job listing for free.