3 ms·

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 l

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.

chlorion 3y ago
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.
- asfarley 3y ago
  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.
layer8 3y ago
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.
- auggierose 3y ago
  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.
  - layer8 3y ago
    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.
    - auggierose 3y ago
      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.
pciexpgpu 3y ago
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.
- auggierose 3y ago
  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.

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.

chlorion 3y ago

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.

asfarley 3y ago
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.

layer8 3y ago

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.

auggierose 3y ago
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.
- layer8 3y ago
  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.
  - auggierose 3y ago
    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.

pciexpgpu 3y ago

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.

auggierose 3y ago
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.