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 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
> 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:
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.
33 comments
[ 4.3 ms ] story [ 80.0 ms ] thread> Pages 165-166: replace all occurrences of "cheese" by "eggs"
Love it
if-nest-a FTW!
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.
Try https://github.com/AndrasKovacs/smalltt if you want a system that considers the things modern systems care about: elaboration and unification.
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.
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.
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 <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.
https://github.com/Z3Prover/z3
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 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.
could you provide example?
>>> 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:
Java has support to run JavaScript code.
>> more people know Javascript than they know C and C++
> this people do UI, and usually not interested in utilizing prover.
JavaScript has been running on server side for 10 years now since NodeJs came out.
Javascripts can be different, there is no guarantee that some half supported engine will run that specific code.
> JavaScript has been running on server side for 10 years now since NodeJs came out.
Same as brainfuck: https://github.com/EvanHahn/brainfuck-web-app
But the point is that potential adaptation could be much higher if library is implemented in C/C++ with bindings to Java/Py/C# and NodeJS too.
Half supported? Where is your source? Java Nashhorn was passing all ECMAScript 5.1 tests in 2012 (https://twitter.com/asz/status/258995374847565825)
> Same as brainfuck: https://github.com/EvanHahn/brainfuck-web-app
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.
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.
Unfortunately, the source code size isn't the main problem with provers. The UX is much more important one.
https://corecursive.com/023-little-typer-and-pie-language/
One effective, if naive, approach to determining whether a logic puzzle has a unique solution is checking:
* is my current constraint set satisfiable?
* if so, exhibit a satisfying assignment ("foo")
* add a new constraint that explicitly excludes the solution "foo"
* is the resulting constraint set satisfiable?
* if not, great! (the solution "foo" is unique)
You could go further towards it feeling like a game, yes -- I've been wanting that too. I'm still learning the basics of these things.
http://incredible.pm/
It's fun!
Admittedly the diagrams tend to explode in size for complicated proofs.