math-comp
coq-simple-io
| math-comp | coq-simple-io | |
|---|---|---|
| 1 | 2 | |
| 548 | 28 | |
| 1.3% | - | |
| 9.1 | 6.8 | |
| 12 days ago | about 1 month ago | |
| Coq | Coq | |
| - | MIT License |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
math-comp
coq-simple-io
-
Inspiring OOP examples?
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".
-
Advent of Code Day 1
It's possible to do all that work still in Coq, so that the extracted code can directly be compiled into an executable. One way is to use the coq-simple-io library, which basically wraps the OCaml standard library (including functions for reading and writing files/stdin/stdout) as Coq axioms. For example, I did extraction that way in a previous iteration of AoC: https://github.com/Lysxia/advent-of-coq-2018/blob/master/sol/day01_1.v
What are some alternatives?
regexp-Brzozowski - Coq formalization of decision procedures for regular expression equivalence [maintainer=@anton-trunov]
proofs - My personal repository of formally verified mathematics.
UniMath - This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
advent-of-coq-2018 - Advent of Code 2018, in Coq! (https://adventofcode.com/2018)
analysis - Mathematical Components compliant Analysis Library
CompCert - The CompCert formally-verified C compiler
coq-library-undecidability - A library of mechanised undecidability proofs in the Coq proof assistant.
advent-of-coq-2021
aneris - Program logic for developing and verifying distributed systems
rupicola - Gallina to Bedrock2 compilation toolkit
magmide - A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.