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.