I wonder about the ethical and legal implications of this work. We've all read and watched sci-fi that warn about the implications of doing this, but biologists agree that reducing diversity within a population makes it much more at risk.

Liquid Types are more limited than "full dependent types" like Lean, Rocq, Agda or Idris. In Liquid Types you can refine your base types (Int, Bool), but you cannot refine all types. For instance, you cannot refine the function (a:Int | a > 0) -> {x:Int | x > a}. Functions are types, but are not refinable.

These restrictions make it possible to send the sub typing check to an SMT solver, and get the result in a reasonable amount of time.

I believe it to be historically true, but Dependent Haskell might change this (https://ghc.serokell.io/dh see unification of types and kinds).

In Lean (and I believe Rocq as well), the Type of Int is Type 0, the type of Type 0 is Type 1, and so on (called universes).

They all come from this restriction.

With respect to Lean/Rocq, that's true, with the subtle difference that Rocq universes are cumulative and Lean's are not.

If it taught them the core concepts of writing good software, that's a win in my book.

Jobs would have kept the button on the bottom, as it's not the proper way to use a computer.

Instead, he would have put motion/light sensors on the screen, so it would automatically wake up when you are sitting in front of it. Macs don't shutdown, they just go to sleep and wake up when you need them.

I think the (hidden) reasoning is that it is really easy to have speedups with slow interpreters. However, getting speedups in high-performance level programs is quite hard, mainly due to micro-optimisations.

That's where the comparison to Python comes from: getting speedup on slow interpreters is not very _relevant_. Now if your interpreter has the same optimisations as Python (or v8 or JVM), even a small fraction of what you show would be impressive.

Having said this, the work your team did is a really challenging engineering feat (and with lot more potential). But I do not believe the current speedups will hold if the interpreter/compilers have the level of optimisation that exist in other languages. And while you do not claim it, people expect that.

He was a poet who could code. Not a software engineer.

(disclaimer: I really like most of his ruby stuff)

Is there any way of measuring how many apps were affected by this change?

Apple crash reports will measure this (if you compare old reports to new ones), but the data isn't public. I assume some third party SDKs will get updates to fix their bugs (and changelog might reveal it) but otherwise it is hard for normal user to see what issue caused an app to crash.

I am looking for more webcomics. Any that you'd recommend to others?

I mostly follow Dilbert and Questionable Content. I used to follow Wizard of Id and a few more, but they also lost support for RSS.

In Portugal it is usually expected that you have one, but every now and then we accept a student without one.

Also notice that in Europe you can get a bachelor and masters in 4-5 years (3+1 or 2), which can be the length of a US undergrad degree.