Boarders on Nostr: In the 80s and early 90s there was a lot of work surrounding the idea of software ...
In the 80s and early 90s there was a lot of work surrounding the idea of software that could assist learning by giving ways of experiencing and visualizing specialized topics often produced by collaborations between content matter experts and programmers - think of the work of Papert (Logo, Mathland), lots of the output of the MIT media lab (including the general tone of SICP which uses lisp to teach something deeper), “Language, Proof and Logic” (https://en.m.wikipedia.org/wiki/Language,_Proof_and_Logic) etc.
In some ways, I think proof assistants serve a similar function in that they are tools for thinking that profoundly transform and expand your world view. Another example is, perhaps, the work of Shiram (+ others) on pyret (though sadly I have not deeply studied it): https://dcic-world.org/
I wonder what other examples come to mind and what a return to these ideas would look like? Or perhaps, now, if the idea is staid and a dead end? In some ways LLMs do the opposite since, even if 100% correct, they operate not as a tool to stretch your worldview, but as a generalized calculator (which is also often sadly incorrect).
In some ways, I think proof assistants serve a similar function in that they are tools for thinking that profoundly transform and expand your world view. Another example is, perhaps, the work of Shiram (+ others) on pyret (though sadly I have not deeply studied it): https://dcic-world.org/
I wonder what other examples come to mind and what a return to these ideas would look like? Or perhaps, now, if the idea is staid and a dead end? In some ways LLMs do the opposite since, even if 100% correct, they operate not as a tool to stretch your worldview, but as a generalized calculator (which is also often sadly incorrect).