this post was submitted on 24 Nov 2023
19 points (91.3% liked)
Advent Of Code
805 readers
13 users here now
An unofficial home for the advent of code community on programming.dev!
Advent of Code is an annual Advent calendar of small programming puzzles for a variety of skill sets and skill levels that can be solved in any programming language you like.
AoC 2024
Solution Threads
| M | T | W | T | F | S | S |
|---|---|---|---|---|---|---|
| 1 | ||||||
| 2 | 3 | 4 | 5 | 6 | 7 | 8 |
| 9 | 10 | 11 | 12 | 13 | 14 | 15 |
| 16 | 17 | 18 | 18 | 20 | 21 | 22 |
| 23 | 24 | 25 |
Rules/Guidelines
- Follow the programming.dev instance rules
- Keep all content related to advent of code in some way
- If what youre posting relates to a day, put in brackets the year and then day number in front of the post title (e.g. [2024 Day 10])
- When an event is running, keep solutions in the solution megathread to avoid the community getting spammed with posts
Relevant Communities
Relevant Links
Credits
Icon base by Lorc under CC BY 3.0 with modifications to add a gradient
console.log('Hello World')
founded 1 year ago
MODERATORS
you are viewing a single comment's thread
view the rest of the comments
view the rest of the comments
I'm currently reading Functional Programming in Lean, hoping to learn enough about the language that I can mange to implement at least the first few riddles in Lean4.
I've set myself the goal that I'll prove to the compiler that all code I write terminates, instead of just throwing Lean's
partialkeyword on functions where the compiler can't prove this automatically...I wanted to do some AoC 2016 riddles as a warmup, but I realized that I'm not good enough in Lean yet to do that, and decided to rather solve the exercises given in the aforementioned book.
I'm optimistic that I'll manage to finish the book still this month, but it's getting tight. I'm now at the beginning of chapter 8 out of 10, but the last 3 chapters deal with those aspects of Lean that are completely unfamiliar to me...
I already don't like it. I know it wasn't a sales pich for the lang, but I'm not sold.
That's the copyright of the book though, not of Lean itself. Lean itself was started at Microsoft too, but is its own open source research project now, with contributions from multiple companies and universities: https://lean-lang.org/about/
But, yeah. Lean can't deny that it was influenced by Microsoft's F#.