Introduction

Warning

Saki-lang is currently in a very early stage of design and development, with substantial work required before it reaches a mature state. The prototype interpreter and REPL are still under active development, and many features are not yet implemented or fully supported. The language design and syntax are subject to change based on ongoing research and experimentation.

Saki is a dependently-typed, pure functional programming language that supports algebraic subtyping and ad-hoc polymorphism. It prioritizes simplicity in design, using a Scala-inspired syntax while leveraging a type system grounded in Martin-Löf Type Theory. Saki introduces novel features like constraint universes and superposition types, serving as a research platform for exploring advanced type systems and verified program synthesis.

Playground

This interactive code playground allows you to write and run Saki code snippets directly in this website. Select a sample program from the dropdown menu or write your own code to experiment with the Saki language.

Example Code: Hello World Example Code: Martin-Löf Type Theory Type Checker Example Code: Red-Black Tree Example Code: Formal Proof of Peano Number

1

/**

Run Code

REPL