stepchowfun/proofs
View on GitHub ↗ ★ 317 Rocq Prover
My personal repository of formally verified mathematics.
5 mentions on Hacker News by 2 people: 1 story, 4 comments · first 2019-02-28 · latest 2023-09-03
20082026
-
…language like Haskell or OCaml, you have the background 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…
comment by stepchowfun · 2023-09-03 · in How to write correct code by construction using the Coq Proof Assistant -
…useful tactic called `magic`) which can automatically prove the theorem from the article. [1] https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor... [2] https://github.com/stepchowfun/proofs/blob/56438c9752c414560...
comment by stepchowfun · 2022-08-01 · in Formally Verifying Rust's Opaque Types -
…as data, universes & other type theory stuff, and extracting verified code—with exercises. [1] https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor...
comment by stepchowfun · 2022-07-17 · in Show HN: A compiler and VM for a simple language, in 150 lines of code -
…book to be impenetrable, so it might not be what you're looking for (I personally love it). [1] https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor...
comment by stepchowfun · 2022-03-17 · in Types versus sets (and what about categories?)