[go: nahoru, domu]

Skip to content

jonaprieto/geb

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Geb Programming Language

CI pages-build-deployment

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.

Who is using Geb?

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.

Documentation

You can find the latest HTML documentation here for the latest version of GEB.

Code Coverage

For insight into our test coverage, you can check out the following:

Quickstart Guide

For those who want to quickly dive in, here's a quick rundown on how to use the GEB CLI.

Installation

  1. Install the Roswell launcher. Remember to add ~/.roswell/bin to your PATH environment variable. For macOS users, this can be done using the following command:
brew install roswell
  1. 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
}

Loading the Geb system

This project uses common lisp, so a few dependencies are needed to get around the code-base and start hacking. Namely:

  1. Lisp with quicklisp.

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

  1. Run sbcl in the terminal:
sbcl .

If sbcl is not installed, you can install it using ros:

ros install sbcl
  1. 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:

  1. Open geb.asd and press C-ck (sly-compile-and-load-file, or swank-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

Formal Specification

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.

Future Key Features

We are currently developing and aiming to incorporate several key features into Geb, including:

  1. Metaprogramming: The capability for programs to generate or alter other programs during execution.

  2. Effects: The approach of separating side effects from the pure part of a program, simplifying code reasoning and testing.

  3. Dependent Types: A powerful feature where types can depend on values, enhancing the expressiveness of the type systems.

  4. Programming Languages and Mathematical Logics as Built-in Types: The unique ability to treat other languages and mathematical logics as intrinsic types.

  5. Composition of Languages and Logics: The amalgamation of languages and logics, with individual components defined as universal constructions.

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

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

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

About

A Categorical view of computation

Resources

License

Stars

Watchers

Forks

Packages

No packages published

Languages

  • Common Lisp 99.8%
  • Makefile 0.2%