4 ms·

Another very small proof system: https://github.com/moonad/formcorejs https://github.com/moonad/formcorejs The core implementation is under 700 lines of JS, in

Another very small proof system: https://github.com/moonad/formcorejs https://github.com/moonad/formcorejs The core implementation is under 700 lines of JS, including the parser: https://github.com/moonad/FormCoreJS/blob/master/FormCore.js 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 https://github.com/kindelia/hvm) and a new proof language on top of that (https://github.com/Kindelia/Kind2 https://github.com/Kindelia/Kind2) with considerably better performance than existing proof systems.

voxl 4y ago
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. Try https://github.com/AndrasKovacs/smalltt https://github.com/AndrasKovacs/smalltt if you want a system that considers the things modern systems care about: elaboration and unification.
- fspeech 4y ago
  I don't understand the allusion to block chains, but I do appreciate the link to smalltt.
riku_iki 4y ago
> 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.
- girvo 4y ago
  > 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.
  - riku_iki 4y ago
    > 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?
    - girvo 4y ago
      > 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. https://github.com/Z3Prover/z3 https://github.com/Z3Prover/z3
      - riku_iki 4y ago
        > 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.
solomatov 4y ago
>The core implementation is under 700 lines of JS, including the parser: https://github.com/moonad/FormCoreJS/blob/master/FormCore.js https://github.com/moonad/FormCoreJS/blob/master/FormCore.js Unfortunately, the source code size isn't the main problem with provers. The UX is much more important one.
- siknad 4y ago
  Small core is easier to verify.

voxl 4y ago

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. Try https://github.com/AndrasKovacs/smalltt https://github.com/AndrasKovacs/smalltt if you want a system that considers the things modern systems care about: elaboration and unification.

fspeech 4y ago
I don't understand the allusion to block chains, but I do appreciate the link to smalltt.

riku_iki 4y ago

> 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.

girvo 4y ago
> 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.
- riku_iki 4y ago
  > 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?
  - girvo 4y ago
    > 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. https://github.com/Z3Prover/z3 https://github.com/Z3Prover/z3
    - riku_iki 4y ago
      > 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.

solomatov 4y ago

>The core implementation is under 700 lines of JS, including the parser: https://github.com/moonad/FormCoreJS/blob/master/FormCore.js https://github.com/moonad/FormCoreJS/blob/master/FormCore.js Unfortunately, the source code size isn't the main problem with provers. The UX is much more important one.

siknad 4y ago
Small core is easier to verify.