See to me Java was an advantage because it ensured I would do part 1 in Not Java (in my case c#). Mind you c# is great because it is similar enough you can follow along while also being different enough that you still are forced to engage and think. At some point I want to redo part 1 in F# to REALLY push myself (and also force me to better engage with F#).
I did the first part in F#, and rather than translating Java to F#, I looked at what the author was trying to accomplish in each step, and did something functionally equivalent in idiomatic F#. That was fun & challenging.
haven't tackled the second part, I'm currently down the rabbit hole with Samuel Mimram's Program = Proof, which I'm just loving and the first book I've seen that focuses on the Curry Howard Isomorphism, covering essential logic, lambda calculus, type theory, and Agda... so good.