I can confirm the TT-RSS app (found on F-Droid) is very good. I have used it for years. On the other hand, the web app is not very good, and each time I wanted to read articles on my computer from the web interface, I encountered huge issues (for some reason, the "right click / mark as read" never correctly worked on my computers, or at least with huge lags of several seconds). When my free TT-RSS provider closed, I decided to switch to FreshRSS and could compare several apps for Android; I finally set up the following workflow: free FreshRSS account + "Read You" (found on F-Droid also), and managed to achieve a very similar workflow than previously (with a much better web app).
Hoare Logic + Dijkstra's weakest precondition + Meyer's Design-by-Contract is what should be used to get LLMs to generate proof with code in a correctness-by-construction approach to implementation.
I’ve practiced array languages extensively myself, including for code golfing, and I fully understand the intellectual joy they can provide. But as I’ve gotten older, I’ve come to see a deep mismatch between what these languages present as “elegant” and what I find truly elegant from a computer science perspective.
Sure, realizing that the foobar of x is nothing more than the transpose of the 15th foo of x, combined via an inner product with the 7th bar of x raised to the power of baz, can be an ineffable intellectual delight. But actually computing that, rather than writing a “boring” loop, feels horrible to me. To my eyes, a “boring” piece of code written by Dijkstra in some Algol-like language contains more beauty than all these dazzling sleights of hand that hide zillions of loops under the rug while pretending that the actual computation doesn’t matter.
On the other hand, whenever I see Python code that does calculations over arrays of data with nested loops instead of using numpy, it always takes me a distressing amount of time to see what the code is actually doing and that the bug is because of a typo buried deep in that 100 lines of code that caused one of the inner products to be incorrect.
It's not like array languages don't do any optimizations... Denying the programmer the ability to be clever by manually writing loops makes some things easier and simpler for the compiler as well.
Array languages are more conceptually simple. What do you concretely mean to mock with:
> realizing that the foobar of x is nothing more than the transpose of the 15th foo of x, combined via an inner product with the 7th bar of x raised to the power of baz
When you compute some nice and elegant result, dissipated heat is an undesired side effect. But let's face it: we are speaking about proof of work. Proof of work means that a computed has run during some "required" time. In other words, you have to prove that enough heat has been dissipated. Waste of energy actually is "by design" here.
I'm not sure if you're trolling. Of course that's nonsense. The work is entirely the (artificially complex) computations necessary to get to the result. If someone were to invent a 100% efficient computer, based on superconductors, which produces no heat at all, the proof of work (the final hash value) would still be equally valid. As I said, heat is an undesired, unavoidable side-effect. You don't show anybody the heat you produced, to convince them that you did the work, you show them the hash value, otherwise you could just burn some wood.
I don’t want to argue about the overall trend based on a single example, but Terence Tao’s substantial use of Mastodon for communication does change the picture a bit.
As some readers may not be familiar with the name Xavier Leroy, I just want to emphasize that he is one of the people behind OCaml and a leading figure promoting Rocq/Coq.
Shameless plug: eight years ago, I created the following website for posting plots of complex functions using similar gradients: https://kettenreihen.wordpress.com/
Those are really cool to look at. I kept trying to click them to learn more, I wish some of them were mini blog posts to give a little bit of grounding.
