> The core implementation is under 700 lines of JS,
why people implement such projects in exotic languages (haskell, JS), and not c/c++, so it can be used in much more wide usecases.
Also, everyone tries to invent some new functional language, while core of prover can operate just first order logic (two quantifiers: exists and any), and on top of that others can build any kind of language to the taste.
> and not c/c++, so it can be used in much more wide usecases.
Because porting a small, simple Javascript library to other languages is typically very easy if you really need it, and C/C++ are a lot more of a pain to implement certain things in?
And I say this as someone who is writing C/C++ (and Nim) daily for work.
If it is a teaching exercise: more people know Javascript than they know C and C++, and there are numerous high-quality provers in C/C++ already that one can use if it's for actual usage, and not just learning.
There are plenty of reasons.
> Because porting a small, simple Javascript library to other languages is typically very easy if you really need it
I want to use some prover lib in my Java/C#/Py code. I can wrap jni API for existing C++ library, or maybe original author already built such wrapper for popular language.
And you propose me instead to go and reverse engineer library Js code which I am not that proficient in, and rewrite all code in Java instead?..
> and C/C++ are a lot more of a pain to implement certain things in?
this is challengeable.
> more people know Javascript than they know C and C++
this people do UI, and usually not interested in utilizing prover.
> and there are numerous high-quality provers in C/C++ already that one can use if it's for actual usage
For example?
Yes, rather than demand others cater to your whims, frankly.
Do you realise how hypocritical it sounds to complain that you are not proficient in Javascript, when others might not be proficient in ?
Go use Z3 if you need a prover in C++ (or Java), its far more robust (provided its the type you're after) than someones 700 LoC JavaScript implementation.