ACL2
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.