Cheese+++
Cheese+++ is set of multiple programming languages which can be nested in one source file and a set of tools for specifying and proving properties about Cheese+++ programs. It is believed to be designed and implemented under a secret project funded by The Big Cheese for a wide range of purposes including but not limited to natural language processing and in particular automated pun development. Cheese+++ programmers call themselves cheesemakers.
Syntax and Semantics
Sequences of the four cheesy codons Cheddar, Brie, Feta, Stilton are used in what's called a culture to build "cheese selections" which undergo coagulation and interact in complicated ways similar to proteins of a genetic code. Cheese+++ programs must be modified to work under different altitudes.
The formal methods toolkit Caerphilly is used for quality control by specifying properties of Cheese+++ programs and then the cheesemakers must work very hard to justify every proof obligation to show the program is valid. Valid Cheese+++ programs can be compiled into a low level assembly language with proof carrying code called Roquefort.
Implementation
The entire toolkit including a pasteurizing supercompiler based on the fourth futamura projection was under development, programmed in Cheese++ but the source code went rotten so it was deleted.