I didn't downvote, I'm just curious who "they" is?
suppose for the sake of argument
1) the Rodin museum wishes to continue receiving funds for culture,
2) the citizen interested in the 3D point cloud has a valid argument (which somehow relies on the fact that 1+1=2)
3) the Rodin museum claims 1+1!=2 and ignores the proof that 1+1=2
4) the democracy had already converted the law into first order logic & set theory form by adding normative or ethical axioms and definitions (it probably even doesn't just define all the axioms and definitions, but even includes example theorems and proofs like "a gypsie also enjoys human rights" or "yes a black human also has human rights" (these would be theorems not extra redundant axioms inserted into the law when this or that extravagant scandal broke out).
With everything set up as above: the citizen asks the Rodin museum for the 3D scans, for some bizarre reason the Rodin museum operators experience an existential nervous breakdown and refuses. The citizen starts assembling a proof that citizens have the right to any data the system generates (besides certain exceptional things like privacy violations or national security). The citizen proceeds to go through the list of exceptions and proves each of them inapplicable (unlike the shape of submarine propellers, the shape of Rodin's statues are not on the national registry of national secrecy). Rodin died in 1917. If any personal privacy data is embedded in the shape of Rodin's statue these people who's privacy is affected are long dead. Any shape modifications that occurred at later dates could theoretically leak private details to the public. Perhaps a vandal inscribed the telephone number of some actress. In that case the Rodin museum is provably a bad custodian, so let's assume the museum was a good Custodian, no privacy violations would occur if they release the 3D shape, and the citizen continues through all the cases and demonstrates no exceptions hold. For some reason the citizen relies on the definition of 2=1+1. If you ask what would probably happen if the Museum just ignores it? It just pretends to be a good museum and decides to sweep the floor again, without obeying to the consequences of the citizen's proof.
Last day of the month, it's Rodin museum's turn to deliver proof of fulfilling their duties, if anyone wants to see pay. They fail to demonstrate completion of all their tasks: that citizen by exercising his provable rights, has automatically inserted a task they refuse to complete. They choose to not earn money... automatically some job positions open, the formally verified government is now looking for a new operator of the Rodin museum.
Thats what I would expect happen if formal verification were embraced in society.
So two issues. Fist, the lack of mathematical rigour in law and policy is generally considered a feature, not a bug. Second, if the state is unwilling to compel action or enforce punishment from/on the entity in the wrong (Rodin in this case) then it does not matter at all how compelling or rigorous the argument is.
Which in Rodin's case is what happened, the author did get a judgement ordering Rodin to turn over the data, they refused, the author then went back to the courts to force them to act. The court decided it didn't want to despite the prior judgement.
It could just be that effect where when you see something once (again) you start seeing it everywhere, but I've seen a recent uptick in administration for old control rooms on the internet recently and I appreciate it.
In the age of digital clouds we've lost the tactile experience of managing the infrastructure we rely on to (IMHO) our own detriment.
I would like to imagine that if pushing a change to production meant a development had to walk down a wall of cabinets with blinking lights toggling chunky switches as they went the simple physicality of the act would be enough to make them pause and wonder if everything really was in order.
It's not even an outlandish ask. We know from say cars that physical interfaces are in some ways more efficient than LCD UIs. It's such a weird thing we don't actually have 24/7 physically staffed control rooms with such indicators and actuators alongside normal displays at large companies
Radar is cheap now, thanks to semiconductors getting smaller and faster the analog front-end which used to be a long expensive chain of components is now much smaller, the ADC is now faster, more accurate, and cheaper, the processor is now fast enough to keep up with a higher bandwidth signal. You could probably drive a very rough radar system directly off a Pico's GPIO and ADC, maybe toss in a decently fast op-amp for a receive amplifier.
Where you will run into issues is processing radar signals into usable data. If you're happy with the results that radar was giving 30 years ago then it's fine and dandy, but the magic of modern radar is in the software, not the hardware.
Someone I know has developed radar hardware, specifically around signal processing, and while they couldn’t say much, my impression from them was that due the very large amount of data involved using off the shelf CPUs would be very limiting, which is why his job for a period of years was developing a design to be put on an ASIC which is significantly more effective at the task.
I feel like it would be unfair to make them include the SVG decoder, the artical uses TypeScript and I believe that is a feature most runtimes (browsers) provide. However they do have to include the SVG files themselves. The Canadian flag from Wikimedia comes in at 699 bytes and France at 262 bytes. So I'm fairly confident that even with compression they'll be over 5kB
We should probably assume that the authors are aware of ceramics, Curie points, and the earth magnetic field. While the article isn't very clear on what effect causes the change in temperature needed to erase the VRM. I suspect is has something to do with how long the object has spent stationary with respect to the earth's field. At least that's my takeaway from having to periodically rotate magnetometers to prevent them from acquiring a bias.
AI inference is basically 1 operation iterated over every single model weight. That's what's makes computer in memory attractive and feasible.
General purpose workloads would require much more silicon real estate and are not (typically) nearly as bandwidth hungry. Just like not all CPU workloads benefit from being adapted to a GPU, even fewer will benefit from being adapted to processing in RAM.
AI is not intrinsically matmul. Current models are a framing of the problem as matmul to enable the bulk operations necessary. There are many calculations that can (and have been) reframed into matrix form to achieve similar results. More than once I have seen a matmul version of something that I thought couldn't have been representable that way. I'm not sure if the greater benefit is the performance or the ability to conceptually manage the problem in you head.
Not all algorithms can be converted of course, but a lot of that is because there are some inherently unparallelizable problems.
Many algorithms can be reasonably converted into matmul. Not many algorithms can be reasonably converted into very low precision matmul. And that's all that these things are going to do.
reply