Getting closer to the event (less than 1 week now!) so figured I would ask this question
Ive been mostly just doing some problems from other years to get used to solving things in rust
I’m not. I don’t plan to speed run it. It’s just a fun activity and part of that fun is just figuring out as I go along.
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…
Copyright Microsoft Corporation 2023
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#.
