Onboard AI learns any GitHub repo in minutes and lets you chat with it to locate functionality, understand different parts, and generate new code. Use it for free at www.getonboard.dev. Learn more →
Top 23 Coq coq Projects
The CompCert formally-verified C compilerProject mention: Can the language of proof assistants be used for general purpose programming? | news.ycombinator.com | 2023-10-27
Also a C compiler (https://compcert.org/). I did exaggerate bit in saying that anything non-trivial is "nearly impossible".
However, both CompCert and sel4 took a few years to develop, whereas it would only take months if not weeks to make versions of both which aren't formally verified but heavily tested.
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.Project mention: Will Computers Redefine the Roots of Math? | news.ycombinator.com | 2023-06-30
For those interested in formalisation of homotopy type theory, there are several (more or less) active and developed libraries. To mention a few:
UniMath (https://github.com/UniMath/UniMath, mentioned in the article)
cubical agda (https://github.com/agda/cubical)
All of these are open to contributions, and there are lots of useful basic things that haven't been done and which I think would make excellent semester projects for a cs/math undergrad (for example).
Learn any GitHub repo in 59 seconds. Onboard AI learns any GitHub repo in minutes and lets you chat with it to locate functionality, understand different parts, and generate new code. Use it for free at www.getonboard.dev.
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.Project mention: Languages on the rise like Rust and Go are being quite vocal against inheritance and many engineers seem to agree. Is this the end of inheritance? What do you think? | /r/rust | 2023-07-04
My personal repository of formally verified mathematics.Project mention: A Taste of Coq and Correct Code by Construction | news.ycombinator.com | 2023-09-03
If you're already familiar with a functional programming language like Haskell or OCaml, you have the prerequisite knowledge to work through my Coq tutorial here: https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor...
My goal with this tutorial was to introduce the core aspects of the language (dependent types, tactics, etc.) in a "straight to the point" kind of way for readers who are already motivated to learn it. If you've heard about proof assistants like Coq or Lean and you're fascinated by what they can do, and you just want the TL;DR of how they work, then this tutorial is written for you.
Any feedback is appreciated!
A function definition package for Coq
Language for high-assurance and high-speed cryptography (by jasmin-lang)
Collect and Analyze Billions of Data Points in Real Time. Manage all types of time series data in a single, purpose-built database. Run at any scale in any environment in the cloud, on-premises, or at the edge.
An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
Mathematical Components compliant Analysis Library (by math-comp)
Formal proof of the Four Color Theorem [maintainer=@ybertot]Project mention: On the Four Color Problem | news.ycombinator.com | 2023-04-07
Takes around 15 minutes on my machine.
A Platform for High-Level Parametric Hardware Specification and its Modular Verification (by mit-plv)
A core language for rule-based hardware design 🦑
A minimalistic blockchain consensus implemented and verified in Coq
Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe]
A library of mechanised undecidability proofs in the Coq proof assistant.
A framework for smart contract verification in Coq
A formally verified high-level synthesis tool based on CompCert and written in Coq.
Convert Haskell source code to Coq source code.
Gallina to Bedrock2 compilation toolkit
IO for GallinaProject mention: Inspiring OOP examples? | /r/java | 2023-03-12
My point about a proof assistant language, let's just say Coq, is focused on pure, referentially transparent functions. There are no IORef like escape hatches required to make things work, although you could probably argue that stuff like this is still pure as, there are certainly escape hatches. Generally speaking, in proof assistants, the program can be self-contained, and is thus "pure".
Program logic for developing and verifying distributed systems
Coq formalization of decision procedures for regular expression equivalence [maintainer=@anton-trunov]Project mention: Show HN: Regex Derivatives (Brzozowski Derivatives) | news.ycombinator.com | 2023-03-07
Thanks for sharing. I am not familiar with Agda. Will take a look. There is somewhat similar code in COQ: https://github.com/coq-community/regexp-Brzozowski
Arity-generic datatype-generic, or doubly-generic, programming in Coq.
SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives
Coq coq related posts
Can the language of proof assistants be used for general purpose programming?
3 projects | news.ycombinator.com | 27 Oct 2023
A Taste of Coq and Correct Code by Construction
3 projects | news.ycombinator.com | 3 Sep 2023
Will Computers Redefine the Roots of Math?
6 projects | news.ycombinator.com | 30 Jun 2023
Recently I am having too much friction with the borrow checker... Would you recommend I rewrite the compiler in another language, or keep trying to implement it in rust?
1 project | /r/programmingcirclejerk | 27 Apr 2023
Inspiring OOP examples?
1 project | /r/java | 12 Mar 2023
There is such thing called bugfree code.
1 project | /r/ProgrammerHumor | 23 Dec 2022
Proofs about Programs
1 project | news.ycombinator.com | 15 Dec 2022
A note from our sponsor - Onboard AI
getonboard.dev | 3 Dec 2023
What are some of the best open-source coq projects in Coq? This list will help you: