> My observation. LLMs find reasoning about Agda as difficult as I find reasoning about C code.

A bit funny, because I thought... Hmm, so LLM's find Agda natural?

My point being... It's a matter oh habit. After writing C firmware for more than a decade, I can read C easily. I might have to think of some parts and trace the code. But I can grokk it and hold the thing in my head. With Rust on the other hand, I just don't feel it as well. I am afraid writing C gave me brain damage and restricted the lens I can see the world through.