Safety

Before we get much further, we should address safety. Safety is a fundamental tenet of Ki; if a Ki program compiles, it is guaranteed to have:

No undefined behavior
Explicitly configured handling of integer overflow (signed and unsigned)
Memory safety
- No dangling pointers (use-after-free, or UAF).
- No buffer overflows
- No multiple deallocations
- No NULL pointer dereferences
- No reading of uninitialized memory
- No use of undefined variables
- No NULL pointers
- No lost pointers (a type of memory leak)
No data races

However, it is possible to do all of these things in another language, and use Ki's FFI library to access that functionality, albeit in a carefully controlled way. This means that Ki is still as potentially unsafe as other languages. One cannot say, "this application is written in Ki, therefore it is safe". One must instead say, "this application is written in pure Ki, therefore it provides all the above guarantees".

Ki is at once a very expressive, yet very strict language. Consider this example:

range DaysInWeek {6}

type ExerciseTracker {
    @field {
        days: array[DaysOfWeek.max + 1]
    }

    fn record_exercise(DaysOfWeek day) {
        self.days[day] = true
    }
}

fn main() {
    day_index: 4
    tracker: ExerciseTracker()

    tracker.RecordExercise(day_index)

    for i, exercised in enumerate(tracker.days) {
        if exercised {
            echo("Hooray, I exercised on day ${i}")
        }
    }
}

The compiler will give an error that, as an int, day_index can index tracker.days outside of its boundaries.

Only a small change is necessary:

fn main() {
    DaysInWeek day_index: 4
    tracker: ExerciseTracker()

    tracker.RecordExercise(day_index)

    for i, exercised in enumerate(tracker.days) {
        if exercised {
            echo("Hooray, I exercised on day ${i}")
        }
    }
}

This is how Ki avoids buffer overflow. This example is easy because it's an array, therefore its size is known at compile time. But what about dynamically allocated arrays (dynarray)?

type ExerciseTracker {
    @field {
        days: dynarray
    }

    fn record_exercise(bool exercised) {
        self.days.append(exercised)
    }
}

fn main() {
    exercise_day: 4
    tracker: ExerciseTracker()

    for i in [0..6] {
        tracker.record(i == exercise_day)
    }

    for i in [0..10] { # Whoops, this is too large
        with tracker.days[i] as exercised {
            echo("Hooray, I exercised on day ${i}")
        }
        else (Error e) {
            echo("Oh no, I got an error on day ${i}")
        }
    }
}

Because the size of a dynarray can only be known at runtime, the compiler cannot use types to ensure that indexes will always be in range. Normally you would use a for-in loop, but the programmer in this example is using a range literal.

In order to safely use indexing in this situation, index operations must be wrapped in a with block, as shown here. In this way, we can separate code that depends on runtime conditions from code that can be statically checked. In this case, the exercised variable is only available inside the with block if the index operation is successful.

Ki also uses with blocks to handle NULL pointers and functions that can fail.

No uninitialized variables

Ki requires all variables to be initialized, in functions, types, structs, everywhere.

No NULL pointers

Ki does not allow NULL pointers.

No pointers to uninitialized memory

This largely means Ki cannot be used by itself to write drivers. That's OK, C is really good for that, and Ki has a great FFI interface.

No globals

There are essentially no justifications for globals, and huge pitfalls. There is no such thing as "global scope" or "program scope".

No out-of-range values

Every scalar has a range, and every potential range violation must be handled. This includes integer overflow, signed and unsigned.

No Aliasing

Only one variable may point to data at any time.

Immutability by default

Variables are immutable by default. Mutable types have their @validate method called on mutation. This allows validation of composite types.

Ki