I agree that functional vs imperative is a red herring in this case.
The Ethereum model is "imperative" anyway, so a functional DSL would probably end up looking like some kind of monad.
That said, it seems interesting to use a language like Agda for writing a DSL to EVM compiler, regardless of the exact nature of that DSL. Then you can have machine checked compiler correction proofs and also prove theorems about DSL programs.
That would be interesting and even necessary. But why not use something much easier than Agda, though not less powerful for this use case -- like TLA+ -- something that even "ordinary" engineers could use to verify their contracts (not to mention that it supports model-checking in addition to deductive proofs, which reduces the verification effort considerably)?
Maybe that would be better. I admit that I don't know the first thing about TLA+. Agda is what I learned about in school, and what my computer science friends are excited about, and I was already interested in using it to write verified compilers. Writing compilers with functional languages was also a part of my university education. But that's just my background.
I see parallels here with UI code that is very imperative in nature, but FRP and similar approaches are showing great promise in creating abstractions for reasoning.
The Ethereum model is "imperative" anyway, so a functional DSL would probably end up looking like some kind of monad.
That said, it seems interesting to use a language like Agda for writing a DSL to EVM compiler, regardless of the exact nature of that DSL. Then you can have machine checked compiler correction proofs and also prove theorems about DSL programs.