larrλtheliquid -> Lemma the Ultimate

An Idealist's journey

This is a live exploration of the question Which languages and formal systems enable the development of trustworthy and understandable software? Rather than trying to come up with an answer in isolation, I publish each step here immediately with little scrutiny. Since this is being done openly and without enough time to develop an ego around opinions, I welcome and am thankful for critical commentary and links to related topics.

Current research project

Reading chapters 1-4 of LCHI to gain a more formal and precise understanding of the basis of Curry-Howard.

Current paradigm hypothesis

External and internal (dependent types) proving of program properties. Statically typed programs with a strong inferencer to make proofs possible but minimize program size. Restricted mutability and total functions for feasibility and minimization of combinatorial explosions in reasoning paths. Curry-Howard isomorphism for compositional proof construction to coincide with compositional program construction.

Current language hypothesis

1. Agda
2. Twelf
3. Epigram