IF the velocity would change from 0.7m/s to 0m/s over one second, the acceleration would be 0.7m/s/s. But if the time span over which that velocity change is (much) shorter, the acceleration would be (much) higher.
Not typically. An airliner can and often does stall just above the runway and then falls the very small distance that remains. So the formula would be more like the airplane falling from a few feet up. The tail is still generating downforce (the opposite of lift) which is why the nose is in the air.
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.
reply