Hacker News new | ask | show | jobs
by sargstuff 7 hours ago
λ-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-draw...

[1] : https://github.com/jeprinz/pantograph/blob/main/README.md

[2] : https://1zb.github.io/3DILG/

[3] : [video] Beyond Lambda-Calculus: Intensional Computation calculus : https://news.ycombinator.com/item?id=49067361

[4] : piet examples : https://www.dangermouse.net/esoteric/piet/samples.html

[5] : esolang Piet : https://esolangs.org/wiki/Piet

[6] : calculus of constructions : https://en.wikipedia.org/wiki/Calculus_of_constructions

[7] : rocq : https://en.wikipedia.org/wiki/Rocq