youtu.be/U3GQePblz4M
What is the easiest language?

Blundered into my first infinite loop bug in Lean - and it seems Lean isn't really as set-up to help rule out certain runtime issues ("panics" and non-termination) as I had initially assumed. A teeny bit disappointed!

I would love a chiller version of AOC where all the problems are first-week level of difficulty.

Day 8 Advent of Code in Lean: github.com/mdr/aoc-2024...

I keep trying to migrate this one and the video gets corrupted. It’s just that powerful!

#FunctionalProgramming #Haskell #OCamel #Programming

React but for TUIs would be fun, I bet that exists already

Day 5 of #AdventofCode in Lean: github.com/chenson2018/...

One of my favorite days so far, came out very cleanly. Having quicksort in the language is nice. I enjoyed writing the function to get the middle of an Array with a provably correct index, though ran into some decidable equality trickiness.

Advent of Code Day 5 in Lean: github.com/mdr/aoc-2024...

Day 4 Advent of Code in Lean: github.com/mdr/aoc-2024...

I suspect I might begin to fall behind the daily pace soon! Today's was a straightforward puzzle, but it took me a while to get both parts working as a Lean novice.

A Shape must be a Circle or a Square. In Scala, I can write

def findCircles(shapes: List[Shape]): List[Circle]

In Haskell (and other FP languages), I'm stuck with:

findCircles :: [Shape] -> [Shape]

Is there a way to achieve the expressivity of the former if you lack subtypes?

Microservices are just technical debt: www.youtube.com/watch?v=LltD...

Day 3 Lean Advent of Code solution:
github.com/mdr/aoc-2024...
I used regexes (but there was enough unpacking of matches that I suspect parser combinators would have been cleaner), and State monad to turn on/off instructions (probably overkill).

Day 2 Advent of Code solution in Lean: github.com/mdr/aoc-2024...

Lean's syntax sugar where you can call certain functions as if they were methods or properties - e.g "report.differences.toSet" - is very pleasant, especially if your day job is OO languages.

I'm trying to learn a little #leanlang theorem proving as well as use it as a programming language for Advent of Code. I would especially like to get to where I could start to prove some simple properties about programs!

🎁 Just in time for your #AdventOfCode puzzles, the latest Unison version, 0.5.29 contains a few code rendering improvements and a hefty performance boost for some programs using the standard interpreter.

I like Lean's Nested Actions syntax
lean-lang.org/lean4/doc/do...

Day 1 Advent of Code solution in Lean
github.com/mdr/aoc-2024...

Just reading the #Lean tutorial. Using special Unicode angle brackets that look visually similar to regular angle brackets is a surely just asking for confusion.