#rocq — Public Fediverse posts

Current status: starting reading chapter 7 of Software Foundation, with #Rocq

So far, I managed to do all the exercises.

Amazing how much *doing*, as compared to only *reading*, helps the learning process.

**Rocq’n’Share 2026**
**Jun 29–Jul 3, EPFL**
Registration free but required: https://framaforms.org/rocqnshare-2026-registration-1769966293
More details: https://proofs.swiss/rocq-n-share/2026/

Are you itching to learn more about the internals of your favorite proof assistant? Do you have a feature to advocate for? Do you need help implementing an extension or hacking the kernel? Do you feel ready to step up and fix that bug that's been pestering you for years?

Join us for Rocq’n’Share! (contd. in thread)

#rocq #rocqprover

TIL the the expression whose value is being "scrutinized" in a pattern match (in #Rocq) is called "scrutinee".

I wrote my first 1000 lines of code of #rocq
I’m impressed that I have just scratched the surface of it.

Yeeee, I completed chapter 1 (of 17) of volume 1 (of 7) of Software Foundation.

It's a long way to the top if you wanna #Rocq and roll.

🚀 Behold the renaming of #Coq to #Rocq, as if the world needed another rocq-solid theorem prover to prove how uselessly rocq-hard #math can be. 🤔 But wait, there's more! Now with extra Polymorphic, Cumulative Calculus of Inductive Constructions, because everyone clearly needs that in their morning coffee. ☕📚
https://rocq-prover.org/about #TheoremProver #Humor #PolymorphicCalculus #HackerNews #ngated

Coq theorem prover is now called Rocq

https://rocq-prover.org/about

#HackerNews #Coq #Rocq #theorem #prover #programming #languages #proof #assistants

Current status: installed #rocq, reading Software Foundation.

RE: https://functional.cafe/@hackuador/116282882755691464

Two more sleeps until the first #BFPG Hack Day of 2026! See yas there, curious minds!

#FP #Haskell #OCaml #Idris #Gleam #Lean #Scala #Erlang #Elixir #FSharp #Clojure #Lisp #Agda #Rocq #Rust #Scheme #Racket

Thanks to Sirius-beta Labs who are once again sponsoring lunch for #BFPG Hack Day. UQ St Lucia, Saturday 28 March. Be there or be a lambda cube!

#FP #Haskell #OCaml #Idris #Gleam #Lean #Scala #Erlang #Elixir #FSharp #Clojure #Lisp #Agda #Rocq #Rust #Scheme #Racket

https://luma.com/uu28az9h

Comparing #Lean and #Rocq (formerly known as Coq)

I thought both were theorem provers, but it seems Rocq is more for building verifiable software, while Lean is for more classical math.

So Lean might be a better fit for the math explorations #LLMs and #AI #Agents are doing for solving problems.

Cylindrical algebraic decomposition in Coq/Rocq. ~ Quentin Vermande. https://dl.acm.org/doi/pdf/10.1145/3779031.3779100 #ITP #Rocq

Readings shared December 29, 2025. https://jaalonso.github.io/vestigium/posts/2025/12/30-readings_shared_12-29-25 #AI #Agda #CoqProver #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math #OCaml #Rocq #SMT

Tacq: Context aware tactic recommendation for Rocq. ~ Jules Viennot, Guillaume Baudart, Emilio Jesús Gallego Arias, Marc Lelarge, Theo Stoskopf. https://hal.science/hal-05428166/document#page=205 #ITP #Rocq

Formalisation de la stabilité de l’erreur d’estimation de l’inclinaison d’un robot. ~ Lynda Bentoucha, Reynald Affeldt. https://hal.science/hal-05428166/document#page=194 #ITP #Rocq

Une sémantique de Kahn mécanisée pour les machines à états. ~ Timothy Bourke, Paul Jeanmaire, Marc Pouzet. https://hal.science/hal-05428166/document#page=17 #ITP #Rocq

Formal verification of Borrow-Checking by local commutation diagrams. ~ Alban Reynaud Michez. https://hal.science/hal-05428143/ #ITP #Rocq

The machine-checked complete formalization of Landau’s foundations of analysis in Rocq. ~ Yue Guan, Yaoshun Fu, Xiangtao Meng. https://www.mdpi.com/2227-7390/14/1/61 #ITP #Rocq #Math

Readings shared December 19, 2025. https://jaalonso.github.io/vestigium/posts/2025/12/20-readings_shared_12-19-25 #AI #ITP #IsabelleHOL #LLMs #LeanProver #Math #Rocq

Prediction: AI will make formal verification go mainstream. ~ Martin Kleppmann. https://martin.kleppmann.com/2025/12/08/ai-formal-verification.html #AI #LLMs #ITP #LeanProver #IsabelleHOL #Rocq

Readings shared December 14, 2025. https://jaalonso.github.io/vestigium/posts/2025/12/15-readings_shared_12-14-25 #AI #FunctionalProgramming #Haskell #ITP #LeanProver #Math #Rocq

A rose tree is blooming (Proof Pearl). ~ Joomy Korkut. https://joomy.korkutblech.com/papers/game-trees-cpp26.pdf #ITP #Rocq

Readings shared December 5, 2025. https://jaalonso.github.io/vestigium/posts/2025/12/06-readings_shared_12-05-25 #ATP #Autoformalization #DataScience #FunctionalProgramming #Haskell #ITP #LeanProver #Math #Rocq #Rstats #SMT #Z3

A Rocq formalization of monomial and graded orders. ~ Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero. https://arxiv.org/abs/2512.04573 #ITP #Rocq #Math

Readings shared December 2, 2025. https://jaalonso.github.io/vestigium/posts/2025/12/03-readings_shared_12-02-25 #AI #CoqProver #ITP #IsabelleHOL #LLMs #LeanProver #Math #Rocq

Readings shared November 25, 2025. https://jaalonso.github.io/vestigium/posts/2025/11/26-readings_shared_11-25-25 #AI #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Programming #Rocq

MiniF2F in Rocq: Automatic translation between proof assistants (A case study). ~ Jules Viennot, Guillaume Baudart, Emilio Jesùs Gallego Arias, Marc Lelarge. https://arxiv.org/abs/2503.04763 #AI #Math #ITP #Rocq #LeanProver #IsabelleHOL #LLMs