GregDavidson

Please share more about this/these quiet group(s). Where can I learn more? I'm also wondering if I already know them!

I can run Maxima on my phone. Heaven!

A UK roundabout us not a European traffic circle or a new traffic calming device. The commentary is conflating at least four entirely different things! A UK roundabout has no place for a decorative feature in the middle. It is a device of ruthless efficiency with typically nothing in the middle but a shiny brass plate in the center set flush with the pavement. Traffic barely slows and rarely stops in the UK, necessitating pedestrian underpasses, Pelican crossings, et al.

I'm delighted this exists as all too many students have used Mathematica in their education and now can't afford it. Yet I'm always wondering why one would write an interpreter for something like this. I've used Maxima much longer than Mathematica has existed. There's no Maxima interpreter or compiler. It's just a read table in Common Lisp. So you're really using CL without needing to know that and some CLs, e.g. SBCL, are extraordinarily efficient. Doing such a thing for other SW tools also gives you seemless interop!

I've been successfully practicing programming with proof of correctness since the 1970s. The confusion I see with most people failing at this is that they're trying to write code first and then prove it correct. The idea promoted by Dijkstra, Hoare, et al is to write the code and the proof together, with each of these aspects of the task supporting the other. The result is (in my experience) a better program developed as quickly (even when not counting on vastly decreased debugging time) as pure coding. Similarly with strong lexical typing: One does not try to create a typing model for a hunk of arbitrary code. Instead, one develops the type model along with the code, with each of those aspects supporting the other. Putting it all together: Coding, Typing (and other Constraining) and Proving are done together, with each of these activities supporting the others. It does take time to learn such a methodology. And it takes extra understanding to maintain types, constraints and proofs as the program evolves, i.e. "maintenance".

Emacs is a Platform. Operating Systems are also Platforms. Many other things are platforms. A platform is a layer of software designed to enable you to build new things on it. This should raise the question: What platform X would be good for building this thing Y I want to build? I often find X = Emacs, but also Racket, Rust, et al. An application which is also a good platform may be worth a greater learning investment than a simpler application would justify.

I use formal verification as part of my development process. The needs of the proof guide the development of the code as much as vice-versa. The result is usually cleaner, simpler, smaller and usually more efficient programs developed much faster as debugging effort is minimal. I still create complete test cases. Proof maintenance as code changes is a pain and I would like LLMs and/or other tools to help with that. I would never try to formally verify code written with regular processes!

I learned to read English the same way I learned to understand it spoken: exposure. As a young child a relative would put me in their lap and a book I liked in my lap and read to me. After awhile I was reading fluently without effort. Most schools teach reading as a conscious intellectual decoding task which leaves little brain power left to engage with the material - the same way most schools teach "foreign" languages. Engage the brain's language centers and language skills will be fluent.

I started with Fortran 2 which has subroutines which don't behave as black boxes. It took me months of frustrated study to understand procedure calls in decent languages as delegation. That opened up the world of high-level computing. Later I would teach this using problems that were a good fit for "recursion". Recursion is not a feature, it's just an obvious pattern of the more general and important nature of delegation. While recursion is occasionally a useful technique, it's tremendously valuable as a tool for learning how to think about procedures as black boxes!

Everything I run on servers I also run on my laptop. Occasionally I get crashes or corruption because of the lack of ECC memory. I'd also like to be able to swap parts between a modular laptop and a home/small-office server, but again - I want ECC. If framework had a model with ECC I'd be all in!

Regulatory systems need omsbuds within the government who can ask for help and explanations from all the agencies regulating a project yet are (primarily) accountable for helping projects succeed as soon as possible and (secondarily) responsible for providing transparent feedback to those agencies and the public where regulation is malfunctioning.

This technology is completely amazing - for large fleet vehicles like buses, trucks, ferries, etc. Also airplanes! Getting this so compact and refined is a technological miracle. Now put it where it fits!

Do what Linus does: Focus on code quality!