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

  • soulsource
    link
    fedilink
    English
    arrow-up
    2
    ·
    1 year ago

    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 partial keyword 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…

      • soulsource
        link
        fedilink
        arrow-up
        3
        ·
        1 year ago

        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#.