I don't hate Lisp, and I definitely don't hate pure functional programming. But I still was motivated to create this alternative. I think there are a few solid reasons why an alternative is valuable.
First of all, ACL2 has a fairly steep learning curve. Generally, I consider myself to have an intermediate knowledge of ACL2 after writing my undergraduate capstone with it, creating two separate iterations of Proof Pad (1, 2), writing a collection of daily projects, collecting and verifying 84 theorems from lectures and assignments, and implementing a pure ACL2 implementation of DrACuLa's utilities, but I still struggle with the syntax and built-in function/macro naming. (Gun to my head, I couldn't tell you the difference between princ$ and prin1$). ACL2 also has many curious omissions, like the lack of built-in reduce, map, and filter functions. Cogito aims to have a consistent, 'batteries-included' library of intuitive builtins.
Secondly, for better or worse, Lisp is not a common language. It doesn't rank in the top 20 in the industry. It's unlikely that undergraduate students will be familiar, and I feel that it's likely they'll spend more time trying to come to grips with Lisp than learning functional programming. (Sure, Cogito also doesn't rank in the top 20, of course. But it's heavily inspired by several languages that do; primarily C(++), Java, and JavaScript)
Perhaps most importantly, I've come to believe that the simplicity of common lisp syntax and parsing is just shunting off complexity onto the programmer. Even adding basic printf style debugging (cw in ACL2) requires modifying the structure of your code, adding new parentheses in hard to predict ways, and probably ideally reindenting your code. In Cogito, it's as simple as adding a print statement on a new line.
ACL2 has made great strides towards being a more expressive general purpose tool in the last few years, introducing loops and lambdas in recent versions. I think that's great, and I make use of both features in Cogito.
This is a peril with every transpiled language when it comes to runtime issues, but arguably worse in the world of ACL2 proof attempts. In general, my approach has always been that: a successful proof attempt is not worth reading, because you're done. An unsuccessful proof attempt is nearly always also not worth reading, because it's so hard to follow, even if you know ACL2 well.
In the longer term, I'd like to use the type inputs to theorems to attempt counterexample production, and I'd also like to explore a reverse transformer from ACL2 output to Cogito like code, but it remains for now as a weakness in Cogito.