Comment by NooneAtAll3

Hmm like the “new” JS Fetch api with `then` chaining? What about map, filter, reduce? Anonymous functions? List comprehensions? FP is everywhere. Pure FP code isn’t seen very often, as side effects are necessary for most classes of programs, but neither is pure OOP code, as not everything is dynamically dispatched, nor imperative code, as Objects or functions may more cleanly describe/convey something in code.

I shoved math aside because I think for most of the HN crowd it wouldn’t be a good use of their time to do what mainstream mathematics is about, like the “things such as Grothendieck schemes and perfectoid spaces” the article also references. FP is much more relevant because for any program for which a proof of correctness is worthwhile, you can always extract a functional core of that program (functional core, imperative shell). And that functional core will be easier to prove than if it were written in an imperative style.

You might like looking at Dafny. It is more imperative focus, but has many of the same software proving functionality that Lean has.

It is different in that it uses SMT instead of dependent types and tactics to prove the software, but I found it more approachable.

Also, it compiles to several target languages, whereas Lean 4 only compiles to C and therefore only supports the C ABI.

FP and math are the same concept.

The semantics of math are equation based.

Everything in the math universal language is defined as an expression or formula.

All proofs are based on this concept.

To translate this into programming think about what programming is? Programming rather being a single line formula is a series of procedures.

  1. add 1
  2. add 3
  3. repeat.

in functional programming you get rid of that and you think from the perspective of how much of a program can you fit into a single one liner? An expression? Think map, reduce, list comprehensions, etc.

That is essentially what functional programming is. Fitting your entire program onto one line OR fitting it into a math expression.

The reason why you see multiple lines in FP languages is because of aliasing.

  m = b + c
  y = x + m

is really:

  y = x + (b + c) 

This is also isomorphic to the concept of immutability. By making things immutable your just aliasing part of the one liner...

So functional programming, one line programs, formulas and equations in math, and immutability are essentially ALL the same concept.

That is why lean is functional. Because it's math.