You don't need to identify the A320 from 15 pixels. Once you see a 15 pixel signature that changes between subsequent frames you point the one extra camera on a movable mount with a 600mm lens on it at it. Now you get a few hundred pixels.
Seeing how the sausage gets made makes you realize ALL the downsides and things you'd rather not have known. That doesn't mean you can think of a way to fix science. Let alone get the required funding to make an actual attempt.
Why mathematicians are three points? I think it is easier to disable a mathematician. Look at this discussion, for example. EE engineers and physicists are dismissing the problem outright, while mathematicians have no issues thinking about it.
For scale: The LHC has more than 11km diameter and the deepest mine we have built is 4km. Adding vertical distance is much harder than making the diameter of the circular tunnel larger.
I worded that poorly, I didn't mean to say that the entire distance should be covered vertically, but rather that a second loop could be wound on top of the first.
It is hard to understand what you mean by type signature, but I think what you mean is something like the type signature in Java, Go or C.
That isn't what people are talking about when they talk about formal verification with a type system. They are talking about much more complex type systems that have equivalent power and expressivity to formal logic.
This intro is good at introducing the topic. Unfortunately, the correspondence between advanced type systems and logic is itself fairly abstract and uses lots of concepts in non-intuitive ways. This means that you can easily wind up in a situation where you can do lots of proofs about number theory using a tool like Lean4, but you don't really see the corresponding types (this is what happened to me).
With dependent types, if you really want to. (Or just with conventional generics or typeclasses, the difference between a ring and a monoid will show, and that's enough for many cases).
If you ignore syntax and pretend that the following is a snippet of Java code, you can declare that a variable x always holds an int, like so:
var x: int = y + 5
Here x is the variable being defined, it is declared to hold values of type int, and its initial value is given by the term y + 5.
In many mainstream languages, types and terms live in distinct universes. One starts by asking whether types and terms are all that different. The first step in this direction of inquiry is what are called refinement types. With our imaginary syntax, you can write something like:
val x: { int | _ >= 0 } = y + 5
Once again, x is the variable being defined, it is declared to always hold a value of type int at all relevant instants in all executions, and that its initial value is given by the term y + 5. But we additionally promise that x will always hold a non-negative value, _ >= 0. For this to typecheck, the typechecker must somehow also confirm that y + 5 >= 0.
But anyway, we have added terms to the previously boring world of types. This allows you to do many things, like so:
val x: int = ...
val y: int = ...
val z: { int | _ >= x && _ >= y } = if x >= y then x else y
We not only declare that z is an integer, but also that it always holds a value that exceeds both x and y.
You asked for the type of a function that multiplies two numbers. The type would look weird, so let me show you an imaginary example of the type of a function that computes the maximum:
val f : (x : int) -> (y : int) -> { int | _ >= x && _ >= y } = ...
This doesn't really get you to the maximum, because f might be computing max(x, y) + 5, but it does show the idea.
The final step in this direction is what are called full-blown dependent types, where the line between types and terms is completely erased.
I was referring to the "The US government is trying to bring back nuclear safety employees it fired on Thursday, but is struggling to let them know they should return to work, NBC News has reported. [...]An email obtained by NBC said the letters for some NNSA employees 'are being rescinded, but we do not have a good way to get in touch with those personnel'." part.
It's about 300 people affected. And when you apply at these types of positions they ARE aware of private contact information.
I really don’t get it. What is the story? Should the employer be shamed for not keeping home/private contact information for all employees? Or is the job of those employees so vital that they could never be considered for firing? The article does not state what their actual occupations are.
>Or is the job of those employees so vital that they could never be considered for firing? The article does not state what their actual occupations are.
They build, maintain and run security for the US nuclear weapons stockpile. This was, in fact, mentioned in the article.
Quote: "The nuclear security officials who were laid off on Thursday helped oversee the nation's stockpile of nuclear weapons. That included staff who are stationed at facilities where the weapons are built, according to CNN."
Would you agree that this is a job of pretty vital importance?
> They build, maintain and run security for the US nuclear weapons stockpile. This was, in fact, mentioned in the article.
That’s what the department does. The article does not say what the erroneously fired employees do.
> Would you agree that this is a job of pretty vital importance?
How would I know? The article does not explain it. To my uninformed ears it sounds like a pretty passive thing, which, if you assume physical security is intact, can keep just fine for quite some time. If they had fired some more vital people, like all security guards, by mistake, surely the article would have said so? But instead the article prevaricates. This makes the article sound untrustworthy.
A sign of WHAT? You still have not explained what the story actually is. When firing 10.000 people on relatively short notice, I would think it unfortunate, but completely expected, if some mistakes were made.
I have no idea. Why are you asking me? The article does not mention it.
EDIT: Or did you mean to say that the article’s story is that the firing was done too quickly? That is actually a decent point, and the article would have been much better if it actually made that point. As it is, the article talks around things, avoids giving crucial details, and relates unconnected facts and pretends to have presented some sort of point, when in fact it only presented the illusion of one.
How is that extortionate? Using the inflation calculator of the Bank of England that is 86 pounds now or $110. Admittedly that more expensive than the current price of $24 for the paper back, but at worst that seems to be twice as expensive as a common price for a 850 page book?
At October, 1970, the provisional figures of average weekly earnings of full-time manual workers were £28 Os. 11d. for men aged 21 years and over, and £13 19s. 10d. for women aged 18 years and over. Between October, 1965 and October, 1970, average earnings of all workers covered by the regular inquiry rose by 45.9 per cent. and the general index of retail prices by 26.4 per cent.
https://api.parliament.uk/historic-hansard/commons/1971/jan/...
So it would have been around a decent chunk of your weekly wage as an average worker, it sounds like. I think what we would need to know is how much excess income someone would have for something like that at the time.
Consider that some technical books have a potential target audience of thousand or so people. Then ask how many hours the book needs to save you to be worth $100. Depending on the book that can look very cheap.
Oh I forgot that's a thing in some countries. I did both of my university degrees just borrowing books needed from the library, they have to have enough copies for every student if needed.
Most of the time we'd end up with a group of friends where we'd each buy a different book then share among each other. Not many were spending the whole amount every semester, especially past the first year when we didn't really know any better.
I think I paid similar for Wolfram's A New Kind of Science back in the early 00's. Huge great beast of a hardback tome, promising the secrets of the universe. I don't think I ever finished it, and ended up giving it away to a charity shop after schlepping it around the world with me, unread.
