11
$\begingroup$

There is a Wikipedia article about non-English based programming languages, but what about for proof assistants?

I recall seeing one which was a translation of Lean tactics to French, by Patrick Massot. I'd love to hear your experiences and thoughts on non-English based proof assistants and their place in society (in the far future perhaps).

Improve this question
$\endgroup$
6
  • 1
    $\begingroup$ Does pp.ipd.kit.edu/projects/brunhilde/brunhilde.php?lang=de count? (note the date) $\endgroup$
    – Sebastian Ullrich
    Commented Feb 9, 2022 at 14:03
  • $\begingroup$ Awesome! That looks really cool $\endgroup$
    – Jia Ming جيا ميڠ
    Commented Feb 9, 2022 at 14:06
  • 3
    $\begingroup$ At least some proof assistants have French names... $\endgroup$
    – Andrej Bauer
    Commented Feb 9, 2022 at 16:21
  • $\begingroup$ What's our general policy on opinion-based questions? $\endgroup$
    – Blaisorblade
    Commented Feb 20, 2022 at 10:44
  • $\begingroup$ @JiaMingجياميڠ What usecases do you have in mind for those languages? Translating Scratch makes sense, because Scratch is used for beginners; but if they stick to programming, they'll struggle to avoid English. In your example, Lean's mathlib is entirely in English! $\endgroup$
    – Blaisorblade
    Commented Feb 20, 2022 at 13:18

2 Answers 2

Reset to default
7
$\begingroup$

The System for Automated Deduction can check proof texts both in English and Russian if I remember correctly: SAD

Translating keywords is of course an easy task, but it'd be interesting to see if there are more fundamental differences in how mathematics is presented in different languages. Most researchers in theorem proving are logicians by training, and logic is usually considered to be universal, but it's probably worthwhile to take insights from linguistics into account when devising languages for theorem provers.

Improve this answer
$\endgroup$
4
  • 1
    $\begingroup$ It's also about access. Peoples who have to learn English as a second language will automatically be disadvantaged, especially if English is not closely related to their home languages and no readily accessible resources are available to them. $\endgroup$
    – Jia Ming جيا ميڠ
    Commented Feb 9, 2022 at 13:40
  • 1
    $\begingroup$ @JiaMingجياميڠ Plain English is not that hard. And much of theorem proving literature is in English. $\endgroup$
    – Gergely
    Commented Feb 9, 2022 at 14:19
  • 2
    $\begingroup$ Sure, from personal experience I agree, but I also think plain Mandarin is not that hard, why don't we all switch to that? ;) $\endgroup$
    – Jia Ming جيا ميڠ
    Commented Feb 9, 2022 at 14:38
  • 3
    $\begingroup$ I would prefer that people instead use plain Lojban instead, but doing that would unncecessarily fragment the PL community, wouldn't it? Many programming languages have keywords/syntax inspired by English, but they are really far from English: English doesn't have an operational semantics but most PL do. $\endgroup$
    – Agnishom Chattopadhyay
    Commented Feb 9, 2022 at 16:04
4
$\begingroup$

I point you to MMP/Geometer, by Xiao-Shan Gao. This system allows you to prove geometric theorems, even through a graphical interface. The commands on the shell are in English, the GUI is mainly in Chinese, the manual is partly in Chinese and partly in English. Theorems are proved automatically via Wu's method, so perhaps MMP can be classified as a computer algebra system or an automated theorem prover, not a proof assistant. However, I'm not sure, because MMP has so many features and I don't know all of them, also because I can't read Chinese.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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