Hacker News Reader

Comment by auggierose | Hacker News Reader

For software like that, not sure how anything other than formally proven correct software is acceptable. And note, no type system is gonna help you with a bug like that.

View on HN

Theory meets practice. An automated theorem proves that knows about Android view hierarchy, Parcelables, Android kernel well really entirety of SELinux not to mention whatever Bluetooth firmware drivers seems quite a bit of boiling the ocean.

The actual device (not the app) does seem poorly engineered and not at all fail safe / provided with ‘might kill the patient’ error handling.

Seems like double whammy where an app and hardware conspire against its user.

In a way you are right, but all that stuff (Android, Parcelables, Android kernel) is garbage. Time to replace all of that with a proper formally proven stack. It's not that Apple or Google don't have the money to do that. They just don't have the will, knowledge and engineers for that.

I don't know very much about formal methods but I would assume the type system plays an important role for encoding that specific states can or cant exist.

But a high reading is a state that can exist. I don’t really see how formal methods would exclude a multiplication/unit error with respect to the displayed unit.

With the right type system, any formal proof can be represented in it, and the type checker will verify the proof. Any fault that remains can also remain with a formal proof. Look up Curry–Howard isomorphism.

Obviously I mean an ML-like type system with automatic inference. Otherwise it is just general logic, and you definitely don't need types for that.

And Curry-Howard is the most overrated isomorphism in history. It may make computer scientists head explode, but mathematicians can live without it.

And yes, I know that Lean is based on it, and Tao is using it, and he just doesn't know better. Sorry.

Type inference is largely orthogonal to the question.

The point is, any formal proof you could do outside a type system you can also do within a type system, so yes the right type system would help you avoid such bugs.

No, that's not the point. There is no point to a general type system without automatic type inference. Because otherwise, it's just a kind of cumbersome and cobbled together logic.

Reply on news.ycombinator.com