Gleam, F# and Lean
11.09.2025 17:32
π 3
π 0
π¬ 0
π 0
Gleam, F# and Lean
![Screenshot of an emacs buffer, the emacs buffer shows:
```
def main : IO Unit := do
let states <- initLeanContext "import Lean
theorem kirans_theorem : β n : Nat, n = n := by
intros n"
let .some initState := states[0]? | return
let mut state := initState
let initialGoals β state.getAllRemainingGoals
println! "\n\n\n\n\n\nInitial state: {initialGoals.length} goals\n\n\n"
-- Apply first tactic
let newState <- runTac state "cases n"
state := newState
-- Work on succ (index 1)
let newState <- runTac (state.setGoalIndex 1) "simp"
state := newState
-- Work on zero (index 0)
let newState <- runTac (state.setGoalIndex 0) "simp"
state := newState
if let .some proofTerm β state.getProofTerm then
println! "Final proof term: {proofTerm}"
-- Demonstrate backtracking
println! "\nBacktracking and trying another proof..."
state := state.backtrack.getD state
state := state.backtrack.getD state
state := state.backtrack.getD state
let newState <- runTac (state.setGoalIndex 0) "simp"
state := newState
-- Show proof term after backtracking
if let .some proofTerm β state.getProofTerm then
println! "Final Proof: {proofTerm}"
```
the other buffer shows a stdout for a terminal and reads:
```
Initial state: 1 goals
After 'cases n': 2 goals remaining
Goals: [case zero
β’ 0 = 0, case succ
nβ : Nat
β’ nβ + 1 = nβ + 1]
After 'simp': 1 goals remaining
Goals: [case zero
β’ 0 = 0]
After 'simp': 0 goals remaining
Goals: []
Final proof term: Nat.casesAuxOn (motive := fun a => _fvar.9 = a β _fvar.9 = _fv (fun h => Eq.symm h βΈ of_eq_true (eq_self 0))
(fun n h => Eq.symm h βΈ of_eq_true (Eq.trans Nat.add_left_cancel_iff._proof_1 )
Backtracking and trying another proof...
After 'simp': 0 goals remaining
Goals: []
Final Proof: of_eq_true (eq_self _fvar.9)
```](https://cdn.bsky.app/img/feed_thumbnail/plain/did:plc:i32jjsch6xqcguzsf2lgbfyu/bafkreiagzuraoyzspf54cw4gumcrtld2n444y5pje4wundtzc7jyuxow7y)
Screenshot of an emacs buffer, the emacs buffer shows: ``` def main : IO Unit := do let states <- initLeanContext "import Lean theorem kirans_theorem : β n : Nat, n = n := by intros n" let .some initState := states[0]? | return let mut state := initState let initialGoals β state.getAllRemainingGoals println! "\n\n\n\n\n\nInitial state: {initialGoals.length} goals\n\n\n" -- Apply first tactic let newState <- runTac state "cases n" state := newState -- Work on succ (index 1) let newState <- runTac (state.setGoalIndex 1) "simp" state := newState -- Work on zero (index 0) let newState <- runTac (state.setGoalIndex 0) "simp" state := newState if let .some proofTerm β state.getProofTerm then println! "Final proof term: {proofTerm}" -- Demonstrate backtracking println! "\nBacktracking and trying another proof..." state := state.backtrack.getD state state := state.backtrack.getD state state := state.backtrack.getD state let newState <- runTac (state.setGoalIndex 0) "simp" state := newState -- Show proof term after backtracking if let .some proofTerm β state.getProofTerm then println! "Final Proof: {proofTerm}" ``` the other buffer shows a stdout for a terminal and reads: ``` Initial state: 1 goals After 'cases n': 2 goals remaining Goals: [case zero β’ 0 = 0, case succ nβ : Nat β’ nβ + 1 = nβ + 1] After 'simp': 1 goals remaining Goals: [case zero β’ 0 = 0] After 'simp': 0 goals remaining Goals: [] Final proof term: Nat.casesAuxOn (motive := fun a => _fvar.9 = a β _fvar.9 = _fv (fun h => Eq.symm h βΈ of_eq_true (eq_self 0)) (fun n h => Eq.symm h βΈ of_eq_true (Eq.trans Nat.add_left_cancel_iff._proof_1 ) Backtracking and trying another proof... After 'simp': 0 goals remaining Goals: [] Final Proof: of_eq_true (eq_self _fvar.9) ```
Finally, a wΜΆeΜΆaΜΆpΜΆoΜΆnΜΆ tool to surpass LeanDojo~
(Creating a Lean Context directly inside Lean itself, and then submitting tactics and backtracking programmatically)
#LeanProver #Lean
@cmuratori.bsky.social⬠gives a compelling analysis of OOP. I wrote production code from the late 80s, using C, which was perfect timing, since OOP has only ever been a thought experiment to me. I like ADTs and DUs, and my new C is #fsharp, which does ADTs better than C.
youtu.be/wo84LFzx5nI
it's a perfectly fine argument to make in isolation, but arguing that *ocaml* of all languages (literally the only language to actually use global type inference) shouldn't have type classes because they hurt *readability* is... something.
There's a lot going on! discuss.ocaml.org/t/announcing... is particularly exciting
Any OCaml devs in Asia???? #functionalprogramming
(Looking for speakers in Asia for invited talks for the OCaml workshop! Women and gender minorities esp!)
Has anyone tried to bring Dusko Pavlovic's work related to "Programs as Diagrams"?
I was in need to build some sketches/specs and most of the visualization tools are not terse enough for me.
Conference presentation slide for FUNOCaml 2025 event in Warsaw, Poland on September 15-16. Features a circular photo of Paul-Elliot Angles d'Auriac, a person with shoulder-length wavy hair wearing round glasses and drinking from a blue cup. The slide announces a talk titled "Slipshow: A Full-Featured Presentation Tool in OCaml" and describes how Slipshow is a presentation tool originally written in JavaScript but rewritten in OCaml, featuring a runtime engine, compiler, collaborative editing website, VSCode extension, and standalone application. The talk explores how OCaml enabled a single developer to create and maintain such a comprehensive project.
Paul-Elliot Angles d'Auriac:
Slipshow: A Full-Featured Presentation Tool in OCaml
FUN OCaml 2025 | Warsaw | Sept 15-16
How one developer rewrote a JavaScript presentation tool in OCaml, creating a platform with runtime engine, collaborative editing, VSCode extension & app.
End of the Indian dream to work in the US.
Tbh, it's a reflection on us. We overvalued their institutions.
It's about time.
Hannes and his peers made their dream a reality by founding a worker-owned collective to write OCaml
and they've been busy building useful things for the ecosystem and for their clients! π«π₯
New Success Story: Secure Internet Services with OCaml and MirageOS π
Robur, a worker-owned collective, builds secure, high-performance, and resource-efficient software solutions!
OCaml's static typing eliminates runtime errors with predictable performance - perfect for system-level programming.
Not arguing. I just didn't know where to stop.
I mean there is a nice summary of E's (print) bias. I didn't want to link it because it's a random medium article.
Since it's well written, claims well sourced
I will not die on this hill but worth thinking about
medium.com/theuglymonst...
Damn jane street cannot catch a break
Damn they keep score, lmao
I cannot in good conscience say it covers the world correctly if it doesn't cater to every day folk.
I don't want to link the article because it's pay-walled and idc. I'll link the criticism to that article which is not paywall and was extensively covered.
www.owenjones.news/p/the-econom...
The Economist, well, has had for at least 19-20 months made themselves loud and clear on who they cater to.
It doesn't cater to me or the third world. This is all too common in western media so I am not surprised.
Genocide in Gaza is a litmus test. Which FT has had better coverage for a while.
FT >>> Economist (rn at least)
I cannot understand this stupid framing as well : bsky.app/profile/shoe...
Legitimizing information that the reader has no opinion about is not revealing information.
If a layperson is reading this every language which is not Java, C, C++, Rust, Python, JS would be obscure.
This seems purposeful and irresponsible to me.
Preconceived notion is harmful for future OCamlers
Why does it keep hammering the image of OCaml being this "obscure" language from the land of France.
Jane street and other trading platforms like Lexifi etc. have been using it for decades.
I don't like when americans inject mysticism in things they don't understand.
I've been having a lot of fun writing an @avaloniaui.net app in #fsharp
This time it got a bit of a lift up thanks to the SukiUI Theme!
We've had this design "on the board" for a while but just put it in a blog post. We're hoping it will help articulate our vision to the #fsharp as well as #mlir and #llvm communities to foster conversation and contribution as more of this surfaces from our lab. speakez.ai/blog/native-...
Damn I was gonna write something similar but now I can use it o7 ty!
Anyone notifying me the regex is wrong didn't get the joke, just saying
Developers reading math :
Let z : A.
By the univalence axiom, the type R(x, z) = R(y, z) is equivalent to the type :
R(x, z) β R(y, z).
"Mathematicians need to learn how to write in simpler ways"
Developers writing regex to filter email address :
^(?:(?!.*?[.]{2})[a-zA-Z0-9](?:[a-zA-Z0-9.+!%-]{1,64}|)|\"[a-zA-Z0-9.+!% -]{1,64}\")@[a-zA-Z0-9][a-zA-Z0-9.-]+(.[a-z]{2,}|.[0-9]{1,})$
"Ah yes, makes perfect sense!"
Is there any org in #Bangalore that would like to lend their space for an #FPIndia meetup? Please dm
#India #FunctionalProgramming #Meetup #Haskell #PureScript #Erlang #Elixir #OCaml #Scala #Clojure
1/ π³DeepSeek just dropped Prover-V2-671B, a 671B-parameter AI model built to tackle formal math proofs in Lean 4. Itβs open-source, massive, and optimized for theorem provingβthink of it as the mathlete of LLMs. Let's dive in π§΅π
Some notes on pathways to join my group at IIT Madras: kcsrk.info/ocaml/iitm/c...