Welcome to Geb, a yet powerful programming language designed with the purpose of providing a universal and unambiguous syntax for defining and translating among any other programming languages. Named in honor of Hofstadter’s iconic work, Gödel, Escher, Bach, Geb is pronounced as a single syllable, adhering to the convention of capitalizing only the first letter, despite its acronymic nature. Dive into Geb and discover an intuitive way to understand, define, and translate various programming languages.
Geb currently serves as one of the backends for Juvix, a high-level, strongly-typed, functional programming language designed for developing general-purpose decentralized applications on the Anoma blockchain. More specifically, Geb is used as an intermediate representation to compile Juvix down into VampIR arithmetic circuits. These circuits are subsequently utilized within the Anoma blockchain through Taiga.
You can find the latest HTML documentation here for the latest version of GEB.
For insight into our test coverage, you can check out the following:
- SBCL test coverage
- CCL test coverage (currently under maintenance)
For those who want to quickly dive in, here's a quick rundown on how to use the GEB CLI.
- Install the Roswell
launcher.
Remember to add
~/.roswell/bin
to yourPATH
environment variable. For macOS users, this can be done using the following command:
brew install roswell
- Install Geb using the Roswell launcher with the following command:
ros install anoma/geb
After these steps, you should be able to run geb
in your terminal.
If you can't run geb
in your terminal, you may need to add
~/.roswell/bin
to your PATH
environment variable. For macOS users, this
can be done using the following command:
export PATH="$HOME/.roswell/bin:$PATH"
Now, let's try running geb
in your terminal with one of the examples
included in the geb
repository:
git clone https://github.com/anoma/geb
cd geb
geb foo.lisp --stlc --vampir --output foo.pir
Here, foo.lisp
is a file containing a valid lambda term. For instance:
(lamb (list (coprod so1 so1))
(index 0))
The output is a vamp-ir expression:
$ cat foo.pir
def *entry* x {
0
}
This project uses common lisp, so a few dependencies are needed to get around the code-base and start hacking. Namely:
-
Emacs along with one of the following:
Assuming sbcl
is installed, one popular implementation of Common Lisp,
and you are in the geb
directory of this repository, follow these steps
to interact with the system using the Common Lisp REPL:
Open the SBCL REPL
:
- Run
sbcl
in the terminal:
sbcl .
If sbcl
is not installed, you can install it using ros
:
ros install sbcl
- Load the system:
(ql:quickload :geb/documentation)
If you're using Emacs, simply run either M-x sly
or M-x slime
,
depending on whether you're using sly
or slime.
To load from Emacs:
- Open
geb.asd
and pressC-ck
(sly-compile-and-load-file
, orswank-compile-and-load-file
if you're using swank).
Once the file is open, you can load the system by writing:
(ql:quickload :geb/documentation) ;; only necessary for the first time!
(asdf:load-system :geb/documentation) ;; if you want to load it in the future
Geb's design is grounded in its specification composed entirely of category-theoretic universal constructions. This enables the portability of Geb-written code across different interpreters. Moreover, thanks to its relatively weak internal logic, Geb can function as a sub-language of nearly any other general-purpose programming language, broadening its compatibility reach.
For more information on the formal specification of Geb, please visit the Geb Specification on GitHub.
We are currently developing and aiming to incorporate several key features into Geb, including:
-
Metaprogramming: The capability for programs to generate or alter other programs during execution.
-
Effects: The approach of separating side effects from the pure part of a program, simplifying code reasoning and testing.
-
Dependent Types: A powerful feature where types can depend on values, enhancing the expressiveness of the type systems.
-
Programming Languages and Mathematical Logics as Built-in Types: The unique ability to treat other languages and mathematical logics as intrinsic types.
-
Composition of Languages and Logics: The amalgamation of languages and logics, with individual components defined as universal constructions.
-
Embeddable within Other Languages: The ability for Geb to be embedded within other host languages, using its effects to call out of the embedded Geb code.
-
Alternative Syntaxes: The existence of a precise specification for functions an interpreter must support, without imposing any constraint on the syntax an interpreter should provide. There will be a correct mechanical translation (an isomorphism) between any two valid syntaxes.
-
Category Theory as Internal and External Language: Geb aims to leverage category theory as both its internal and external language, providing access to the broad domain of functions and theorems developed in category theory since its inception.