[Agda] Background reading?

[Yakov Zaytsev]

Could you suggest books to learn how to program in Agda2?

AFAIU Agda2 is more about theorem proving then usual programming
like in Haskell for example

I've found it hard to pick up right curriculum for logic and proof theory for
beginner

Girard mentiones Proof Theory and Logical Complexity in Proofs and Types
book
Is it a good starting point?

I mean words like logic tactic horrifies me :-)

TIA