Galo JS is an attempt to make a js proof assistance.
The project is somehow inspired by other existing proof assistance programs, my favorite is Coq (http://coq.inria.fr/).
My motivation to this project is to learn more about proof concepts but also to make a proof assistance that is closer to a mainstream programing language like JavaScript.
The goals of the project are:
- Use a pure formal mathematical representation to represent a program, I will call this representation as L,
- L has to be pure JavaScript language so it can be accessed, manipulated and extended by normal JavaScript code. So all core functionality should be a collection of JavaScript libs,
- Completely translate JavaScript language to L,
- Build mathematical correct libs on top of L that would help on program validation,
- All L core libs should run on browser and nodejs,
- Build a interective browser IDE, with offline support, that would be easy to test and exepriment with all the above ideias,
As a test case lambda-calculus had been choosen to be L.
Afther getting the repo code:
- The index.html let you try all the code interectivly, everything is acessible by js and is evaluated in real time,
- The print function is used to print a string to the rigth console in index.html,
- Everything that can be transformed to a string can be printed for example: for (i in Lambda) { print(i); } will print the Lambda dictonary keys.
- For using the libs check the index.html.
The project is called galojs for the following reasons:
- JS stands for JavaScript,
- Galo it's the word translation of Coq, the name of a very good/cool proof assistance program, to Portuguese,
- Galo it's a Portuguese national symbol ("Galo de Barcelos"),
- Galo it's Portuguese slang for a bump in your head (witch is how I feel when I think on this stuff),
- Cock is a animal that is always trying to proof himself,
- Cocks are like penguins they are birds that can't fly, except they can fly a little...