Kip

A homotopy type programming language with a web-based syntax tree editor.

Kip is named after the Kenyan long-distance runner, Eliud Kipchoge, who has all the qualities we want in a program. Moreover, Kipchoge is a phenomenal human being to be honored.

The limits of my language means the limits of my world.

― Ludwig Wittgenstein, Tractatus Logico-Philosophicus

Ambitious projects, like AR/VR and robotics, are limited by the programming languages we use. To make AR/VR possible, we really need a platform that combines symbolic computation (Wolfram, proof assistants), scientific computation (Matlab, Julia, NumPy), and graphics programming (OpenGL, WebGL, Vulkan). Such ambitious tasks demand an all-encompasing language capable of embedding domain specific languages (DSLs), e.g., Lean 4 allows for elaboration of custom syntax categories.

The problems are solved, not by giving new information, but by arranging what we have always known.

― Ludwig Wittgenstein, Philosophical Investigations

It is high time that we united math, physics, chemistry, and engineering into one single framework, and create a global computable knowledge database. Children could learn most STEM subjects in this unified framework and carry those experiences throughout their adult career. This would also enable AI to learn how we humans do STEM work, and allow AI to produce reliable STEM work. What we want is some sort of Wolfram-mathlib4-CubicalAgda-ATS2-SPARK2014-CompCert-seL4-LyX-Squeak/Smalltalk-lamdu-SemanticDB hybrid.

Every now and then a man's mind is stretched by a new idea or sensation, and never shrinks back to its former dimensions.

― Oliver Wendell Holmes Sr., Autocrat of the Breakfast Table

We hope to stretch minds, especially young ones, with homotopy type theory and a new paradigm of syntax-tree-based WYSIWYM editing.