I don't know Ruby, and I'd argue it has dissimilar syntax to many other languages I use regularly (that's changed over the years but whatever, my point still stands).

I can still read ruby code, because it's still readable. Same with Lisp, which I never bothered to sit down and learn until about a year ago. Prior to that, I still had no problem reading and understanding it (perhaps not as intuitively as someone who writes it regularly).

The quoted example is, for all intents and purposes, gibberish to me. And I have worked with CoQ.

Well, and to me this syntax makes sense intuitively. And to most beginner programmers, all code looks very hard to understand. I'm really bad at understanding pgsql, I dont't like it at all. People just have different experiences.

Ruby still has algol-like structure, like most common languages. And basic lisp syntax is "normal" function calls with the parens moved around.

Of course, some things are objectivly more complex than others, but making that argument here requires a bit more evidence.

I'm with you about all code is difficult to beginners. About language designers, they should decide who they want to address with their language and how popular they want it to be. If they want to become mainstream and they don't have a way to force people to use it (example: Apple with Objective C and Swift) then they should make a language with a syntax similar to something already mainstream. Example: Elixir got reasonably popular and in its early days it was common to think about it as a functional Ruby. It is not. Anybody using it would find it very different from Ruby by the end of the first day. However there is at least a correspondence between many Module.function / Class.module names in the standard library and the same do / end general structure of code blocks.

My advice to any language designer aiming to mainstream status is to copy some curly braces language (Java, JS, C++) or Python. Then do any weird thing to them, but don't scare away millions of developers with your hello world.

Coq is quite readable imho. I work mostly with k, Ocaml and Haskell (trading); I find ruby unreadable. I find it extremely ugly and my brain simply sees it as line noise, while k (and Egison by the way) reads fine. Each their own, I guess.