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.

This game (still) rocks.

I binge-completed the first four chapters some time in 2014, did the next four in 2016, and then sadly let the project of finishing "Software Foundations" sit idle for almost ten years. :(

Well, any time is infinitely better than never, so here I go with the significantly expanded 2025 edition!

https://softwarefoundations.cis.upenn.edu/

Image warning: Screenshot spoils the solution to one exercise.

#coq #rocq