Is there a Proof assistant which also is an esoteric programming language? If so, then how many there are, approximately?
$\begingroup$
$\endgroup$
3
-
8$\begingroup$ I think a cynic might argue that theorem provers form a proper subset of esoteric programming languages ;) $\endgroup$– Alex NelsonFeb 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$– Nike DattaniFeb 9, 2022 at 21:17
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
- 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
gccto check proofs for me. This satisfies the "hard to program in" criterion.
