The hype of Blockchain is an astounding thing, and the cascading hype for systems merely because they are based off people in the Blockchain space is equally as befuddling.
> 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.
> 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
Brainfuck? JavaScript is one of the most popular programming language (https://www.stackscale.com/blog/most-popular-programming-lan...) You're comparing apples to oranges. By the way I mostly work in Java, but I do not look down on JavaScript, it's shows ignorance.
As others have already said, person who wrote the library may not be familiar with your favorite language, moreover certain things are easier to do in some languages. This is not the attitude that we should be showing when receiving free work from someone. If you don't want to port it to your favorite language when needed that's ok, I'm just glad that it exists.
> Java Nashhorn was passing all ECMAScript 5.1 tests in 2012
Half supported means it is some Mozilla side project which likely is not funded.
> JavaScript is one of the most popular programming language
it is popular on UI yes, for backend I am not sure about that.
> person who wrote the library may not be familiar with your favorite language
he/she could create it as a throwaway weekend toy project, without interest in wide adaptation and high impact, yes. Also, my critics was directed not to him/her specifically, but to the fact that all other do the same.
> moreover certain things are easier to do in some languages.
this is not about implementing prover n javascript
> This is not the attitude that we should be showing when receiving free work from someone.
My attitude is that I am entitled to express opinion if it is well justified.
> 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?..
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 <insert your favoured language here>?
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.
> Yes, rather than demand others cater to your whims, frankly.
everyone caters their own part. I am giving suggestion how to cater more people, but if author is not interested in wide adaptation, it is his choice. I am more wondering why such behavior is so common.
> Do you realise how hypocritical it sounds to complain that you are not proficient in Javascript, when others might not be proficient in <insert your favoured language here>?
Not favorite, but language convenient for usage from other languages.
> Go use Z3
z3 is sat solver, which is very different to theorem prover.
Theorem prover in C is eprover for example, but it doesn't provide convenient API.
> I am more wondering why such behavior is so common.
I have already explained why it is common. Your dismissal of those explanations is neither here nor there, frankly. Most of these are example libraries done in the languages they know, not production quality systems for you to integrate. It's basically that simple.
And yes I'm aware re. Z3, which why in my quote I specifically said "provided its the type you're after". There are other choices across a range of languages, which a quick google search found. And Z3 is more than just a pure SAT solver, too.
>>> ctx.eval("var x = {company: 'Sqreen'}; x.company")
although it doesn't give much clue how I install npm for referenced prover.
Another story is that referenced prover is not just prover implemented in HS, it is some compiler of functional language, so you would need to call Pyminiracer from your py, which calls some JS function, which will receive code in that functional language:
This is a very good book that will teach you the basics of manipulating code in a correct way (correct as in mathematically correct, not in some nebulously ill-defined level of correctness).
The core implementation is under 700 lines of JS, including the parser: https://github.com/moonad/FormCoreJS/blob/master/FormCore.js
The author has since moved on to building a runtime with optimal evaluation (https://github.com/kindelia/hvm) and a new proof language on top of that (https://github.com/Kindelia/Kind2) with considerably better performance than existing proof systems.