The Toaster Programming language

Toaster is an experimental programming language where I can experiment with trendy new language features. The focus of Toaster is on language features with minimal overhead and type-safety.

The language features that Toaster has or will have are as follows.

• C++-style function overloading: Function overloading in C++ has notable, desirable properties. First, function applications are resolved statically. Second, it relies on a metric for selecting the best of multiple viable functions.
• Predicate logic: Toaster avoids abstraction overhead by bolstering its type system with a logical system. This is inspired by the Liz programming language.
• Compile-time evaluation and partial evaluation
• Extractable proof obligations: The semantics of Toaster are modeled in Coq. Logical assertions made in code can be extracted as proof obligations in Coq.