jupitr

I feel the lisp constructed on top needs significant language expertise. Lispy constructs of defvar, defconst, defcustom, alist, cl-loop etc. are quite extensively used in emacs - and need an understanding quite unique to Lisp. Of course, the domain then builds on top of this shared understanding of the contructs themselves.

I would say that loss of expertise in emacs-lisp is a significant loss, even if there continues to exist C-expertise globally.

This is the same idea as the fixed point of the meta-circular evaluator - the abstract ideal language that lisp models almost exactly.

the capture-pane, send-keys, set synchronize-panes on/off are somewhat difficult to pull off when targeting one terminal from another. For scripting or even simple functions that depend on multiple terminal states, being able to reliably read and write to a terminal become rather essential primitives.

this feels like excellent foundations for a board game. fascinating!

It's not necessary, but is significantly more radio-quiet than a lunar orbit. And secondly, though unfortunately not something we could really exploit this time, the stable temperatures of the lunar night greatly help with calibration for sensitive measurements like the 21cm Dark Ages signal

This is quite seriously missing the point: computational theorem-provers and contributions to mathlib (for Lean, anyway) allow for checking "correctness". The LLM is one of the many ways to search for tactics that help complete a proof for a theorem not yet in mathlib.

The LLM is not done until the theorem-prover says it is done - at which point we can be sure of the correctness of the assertion in the context. AFAIK there is no debate about inaccuracy with theorem-provers. Their real limitation continues to be converging in realistic timescales and efficient search over all combinations of proof tactics.

makes me wonder if a sufficiently large number of connected nodes can represent bits via their online/offline status, and their network graph representing "memory"

How was the interactivity achieved? Could you maybe link to the source so I can learn? I have been trying to get something like this working with quarto, but it is getting way too complicated.

and also how to lie with visual proofs: https://www.youtube.com/watch?v=VYQVlVoWoPY