zlacker

> It would be neat to have an image-based runtime like Commmon Lisp or Pharo (SmallTalk) while the language is statically typed in a rich system like Lean that can generate optimal native machine code and GPU shaders, etc. A fast, interactive theorem prover is also a must. If I’m gonna have my cake and eat it too might as well go all in.

What is stopping you from working on this?

>>willia+(OP)
Time and money. Get me funding enough for myself and another dev and some customers and let’s go.

>>agentu+H7
My dream project, if I ever win the startup lotto and come into some "mess around and find out," money, would do one better: let's not even require a graphical display or keyboard input.

My personal goal here is to be able to write my programs by synthesizing them from proofs that I write by hand. Whether that is on a special device like an eInk reader or on a whiteboard; my work carries around with me where I choose to take it. I would love a world where my physical attention isn't focused on a glowing box with graphics designed by some company in Palo Alto or Cupertino who is designing for mass audiences with profits motivating every decision (and change). Why even hard-wire ourselves to the physical legacy of terminals?

There are plenty of humans who aren't even afforded access to modern computers in manners that are convenient to them and respect their abilities and capacities! The entire design of modern computing is centred around able-bodied, able-minded "mass-market" people -- whatever that is.

It's frustrating that any other mode of computing is an after-thought, an inconvenience, and attached to these machines in order to meet people where they are. Often times the answer is simply, "Nope, sorry."

Particularly inspired by: DynamicLand, https://screenl.es etc

>>agentu+Od1
Thanks for introducing me to DynamicLand and Screenless!

DynamicLand reminds me of early Logo where there was a physical "turtle" robot that kids programmed to draw on paper!