λ-2D: An Exploration of Drawing as Programming Language, Featuring Ideas from Lambda Calculus [0] One can use intensional calculus concepts to model non-lambda

λ-2D: An Exploration of Drawing as Programming Language, Featuring Ideas from Lambda Calculus [0] One can use intensional calculus concepts to model non-lambda languages[3]. A live 'CoC'[6] / rocq[7] layer to hightlight/note 'correctness' issues (auotmated suggestion of proof of correctness/unresolved ANTLER freevars take on ast editors 'valid' language statement(s)/language block(s)) ast editor with gui nodes (panograph[1]) / code block with "user shape" construction using 3DILG[2]? 3d bar codes could be taken as a 'multi-statement' token. Piet[4][5] programming language might be more useful than 3d barcode as langauge token though (condensed spreadsheet). ----------------------------------------------------- [0] : https://www.media.mit.edu/projects/2d-an-exploration-of-drawing-as-programming-language-featuring-ideas-from-lambda-calculus/overview/ https://www.media.mit.edu/projects/2d-an-exploration-of-draw... [1] : https://github.com/jeprinz/pantograph/blob/main/README.md https://github.com/jeprinz/pantograph/blob/main/README.md [2] : https://1zb.github.io/3DILG/ https://1zb.github.io/3DILG/ [3] : [video] Beyond Lambda-Calculus: Intensional Computation calculus : https://news.ycombinator.com/item?id=49067361 https://news.ycombinator.com/item?id=49067361 [4] : piet examples : https://www.dangermouse.net/esoteric/piet/samples.html https://www.dangermouse.net/esoteric/piet/samples.html [5] : esolang Piet : https://esolangs.org/wiki/Piet https://esolangs.org/wiki/Piet [6] : calculus of constructions : https://en.wikipedia.org/wiki/Calculus_of_constructions https://en.wikipedia.org/wiki/Calculus_of_constructions [7] : rocq : https://en.wikipedia.org/wiki/Rocq https://en.wikipedia.org/wiki/Rocq