a little program in a little-known, little-documented language called ATS.
some undocumented features i found while looking through the source code of the proof language beluga.
a solver for digitle (numbers countdown) in maude, a language for rewriting systems.