Skip to content
Systems Programming meets Verified Programming, a highly WIP Programming Language
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
src
.gitignore Initial Commit Feb 13, 2019
Cargo.lock Resolve waiting references once modules are added Feb 26, 2019
Cargo.toml
LICENSE.txt License: MPL 2.0 Mar 27, 2019
README.md

README.md

alox prototype

Systems Programming meets Verified Programming

This is very much a Work In Progress, nothing works yet.

Here's a roadmap:

  • AST to IR conversion
    • AST Structure
    • Thread-safe IR Structure
    • Concurrent IR Symbol Resolution
    • AST Expression -> IR Instruction conversion
    • Passes to validate things
  • Lexer & Parser
    • Start parsing needed files immediately
  • Error messages
  • Backends
    • Look at CraneLift
    • LLVM
  • Really dig into semantics

Language Ideas

  • Pure code by default
    • Allows for compile time code execution
    • Permission based system - +IO, +Syscall, +MutateArgs
  • Strong type system
    • Algebraic Data Types
    • Refinement Types
    • Unique & Borrowed Types
  • Automatic Versioning
    • Enforce public APIs
  • Clean syntax
  • Concurrent compiler pipeline
let INT32_MAX: Int32 = 2_147_483_647

fun bounded(n: Int32): Bool
let bounded = (n) -> { 
    return (addWithOverflow(n, INT32_MAX) > 0) && (n < INT32_MAX)
}

// add function that can't overflow at runtime
// 'bounded' can be used because it is a pure function
fun add(x: Int32, y: Int32): Int32
    where (y: bounded(x + y), return: x + y)
let add = (a, b) -> {
    return a + b
}

import std.io

// println requires the caller to be annotated with +IO
fun main() +IO
let main = () -> {
    let a = INT32_MAX - 2
    let b = 3
    // compile time error!
    let c = add(a, b)
    io.println(c)
}
trait Action {
    fun action(): Int32
    fun otherAction(): Int32 +MutateSelf
}

struct Container : Action {
    let x: Int32
    let y: Int32
    
    // function declaration is taken from the trait
    let action = () -> {
        return self.x + self.y
    }
    
    // this function is allowed to mutate itself
    let otherAction = () -> {
        self.x = self.x + 1
        return self.x
    }
}

fun main() +IO
let main = () -> {
    let container: Action = Container { x: 1, y: 2 }
    container.action()
    container.otherAction()
    io.println()
}

Inspired by Rust, Liquid Haskell, & many more.

You can’t perform that action at this time.