pantograph

λ-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

Currently, we've only instantiated the system for the simply-typed SML-like language that you can use in the tutorial (https://pantographeditor.github.io/Pantograph). Going through that tutorial will also give you a tour of the language features in there. The next phase of work is on instantiating more complicated languages and type systems, to see how the framework can be extended. In theory, a lot (such as the entirety of SML) could be instantiated currently, but it would be quite cumbersome (here's what the implementation of the currently instantiated language looks like https://github.com/jeprinz/pantograph/blob/main/src/Language...). So we're working on trimming down the formalism and developing new abstractions to make things easier, and to support some more advanced typing systems that actually would have problems with the current

Thanks! We're working on extending the system to support more advanced type systems. In theory, the current system could already support these kinds of features (but not in quite as slick a way as modern languages, most likely), but it would be very cumbersome, so the work is in trimming down the formalization and taking advantage of new abstractions. Check out the implementation for a look at how defining the actual language (and typing rules) works currently https://github.com/jeprinz/pantograph/blob/main/src/Language...