Advent of Code 2025

[Bryan Hunter]

Advent of Code started today! 
https://adventofcode.com/2025

Feel free to play along with the group by pushing your FP solutions here:

https://github.com/NashFP/advent-2025

Every year Advent of Code is what makes the holidays feel real for me. I'm going to try to solve each with Elixir's Nx library this time. Love to hear your plans.

Wishing you all a peaceful, happy, nerdy December.

-Bryan

[Jason Orendorff]

On Mon, Dec 1, 2025 at 5:23 PM Bryan Hunter <bryan....@leanfp.com> wrote:

Advent of Code started today! 
https://adventofcode.com/2025

Feel free to play along with the group by pushing your FP solutions here:

https://github.com/NashFP/advent-2025

I have been taking this as an opportunity to learn Lean, a purely functional language with dependent types and proofs, like Rocq.

More about Lean: https://lean-lang.org/learn/

My beginner code: https://github.com/jorendorff/advent-of-code/tree/main/2025

Lean is a Very Large language, like Rust or Common Lisp, not small like C or Scheme. The core of the language is the same as Rocq as far as I'm qualified to say, but it's more oriented toward actually building and running real programs. It seems to have picked up some nice superficial bits from Elixir, like the `|>` operator and `ModuleName.funName` syntax for organizing related functions. The interesting tension in the language is between actually carrying around proofs, which is very time-consuming and prone to dead ends, but produces theoretically verifiable programs; or not, in which case you might as well use OCaml.

I haven't successfully proven anything about my programs. Just getting them to run is hard enough!

You know, since there are only 12 puzzles this year, we could have a recurring feature of NashFP in 2026: someone (or someones) present their solution for the corresponding day's puzzle... So in January, we do Day 1; in February, Day 2; etc. Although, we only have 11 meetings a year, not 12. It almost lines up. Hmm.

-j

[Mark Wutka]

I'm doing decidedly non-FP solutions this year, I'm doing them in Ada/SPARK for a charity thing that AdaCore is doing where they donate money to the Ada Developers Academy for each Ada or SPARK solution. The Ada Developers Academy is not actually about developing in Ada, but like the language is named for Ada Lovelace and provides training for groups of people who are traditionally underrepresented in Computer Science.

I'm doing my code in SPARK, which involves running a prover to prove that my code contains no runtime errors. Most of the time I do not have to write assertions (pre/post conditions, invariants), I just write the code in a way that avoids the possibility of overflows or array bounds exception. Occasionally I have had to declare loop invariants to help it prove things about values that change in a loop.

--
You received this message because you are subscribed to the Google Groups "Nashville Functional Programmers" group.
To unsubscribe from this group and stop receiving emails from it, send an email to nashfp+un...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/nashfp/CAPh8%2BZoOF1RzMS4gbtoFYtu6qTREvCXJ5MjBhTCzHae4G_2KUA%40mail.gmail.com.

[Tim Dunnington]

I had to learn Ada in college. I was at U of MD, and being close to federal gov't, they decided to make Ada a required language.

I'll be curious to see your solutions!

I went with Clojure this year myself but I hardly have time so...only go through day 1 lol! But hey it's a start :)

Happy holidays y'all!

To view this discussion visit https://groups.google.com/d/msgid/nashfp/CA%2BvyaX2BgpP72n0zZa_eqYeUSPGipXn%2BzBEDa%3D4r4v5nDzuyGw%40mail.gmail.com.

[Mark Wutka]

I also learned Ada in college. I was at Georgia State, and it was also because of the DoD Ada mandate. They supplied free copies of the Janus Ada compiler.. on 5 1/4" floppies. I didn't have a hard drive, so I would put the disk with my Ada source in drive 2, and then I would have to swap 4 different disks in drive 1 to compile and link.

My solutions are here:
https://github.com/wutka/advent-of-spark-2025

There other folks who have more concise Ada solutions. Because I am using SPARK, I often avoid external libraries except for sparklib which has formally proven containers, and a binary heap implementation that I wrote myself. I also do all kinds of bounds and overflow checks, so it can be tedious to read.

To view this discussion visit https://groups.google.com/d/msgid/nashfp/4ff169b4764fde6bc2405701e61178cb6b466c9f%40hey.com.

[John Wise]

If you want to cheat<bs><bs.>ck. This guy is walking through using Clojure in the form of Clerk notebooks.Advent of Code 2025