ACL2 (A Computational Logic for Applicative Common Lisp) is a programming language based on Common Lisp and supported by a theorem proving system. It is primarily used for formal verification of properties and correctness of computer systems and software.

Hello, world code example:

(cw "Hello world!~%")

Popularity: Less than 1% of developers are using or have used this language.*
*According to StackOverflow's 2023 survey.