Is there a Proof assistant which also is an esoteric programming language? If so, then how many there are, approximately?

  • 8
    $\begingroup$ I think a cynic might argue that theorem provers form a proper subset of esoteric programming languages ;) $\endgroup$ Feb 9, 2022 at 20:07
  • $\begingroup$ We do have checkers for CoC whose code fits on a postcard and stuff like that :) $\endgroup$
    – Trebor
    Feb 9, 2022 at 20:09
  • 4
    $\begingroup$ I upvoted because I don't think this question needs to be downvoted, but I'm sorry to say that I close-voted since the community overwhelmingly didn't like it being open. 1-line questions in general tend to be poorly received, so some advice for the future would be to focus more on the quality of the question. $\endgroup$ Feb 9, 2022 at 21:17

1 Answer 1

  • Falso, by Estatis Inc. is perhaps technically an esoteric programming language, fitting into the "designed [...] as a joke" category.
  • I've occasionally thought about how to leverage C++ templates (which do sort-of support dependent types) to get gcc to check proofs for me. This satisfies the "hard to program in" criterion.

Not the answer you're looking for? Browse other questions tagged or ask your own question.