3 ms·

Demistify what? Modern code is a construct of patches over patches over hard-coded parameters that nobody understands how it works as a whole and nobody dares t

Demistify what? Modern code is a construct of patches over patches over hard-coded parameters that nobody understands how it works as a whole and nobody dares to put it through formal verification. Airplanes crash, money is lost, data is stolen but nobody seems to care. So we will keep winging it.

afarrell 4y ago
> Airplanes crash...but nobody seems to care If you think that nobody cares when airplanes crash, that signals that you likely want to: 1. Re-evaluate the evidence. Boeing was fined $2.5 Billion[1] over the MCAS debacle after it was a major news story. 2. Talk to someone about burnout. Cynicism is one of its major symptoms[2]. [1] https://www.justice.gov/opa/pr/boeing-charged-737-max-fraud-conspiracy-and-agrees-pay-over-25-billion https://www.justice.gov/opa/pr/boeing-charged-737-max-fraud-... [2] https://alifeofproductivity.com/remember-burnout-and-cynicism-go-hand-in-hand/ https://alifeofproductivity.com/remember-burnout-and-cynicis...
astrange 4y ago
Airplane code certainly is put through “formal verification”, but also “putting it through formal verification” is not a magic spell that removes bugs from a program. It only proves it does what is in the spec. It seems like the word “formal” impresses people too much.
- oldgradstudent 4y ago
  > It only proves it does what is in the spec. Worse than that. Usually, it only proves that a simplified version of the code satisfies to some extent a translation of the spec to some formal language. And "prove" only means that some rather buggy tool printed "Valid". Every point in this chain can and often does introduces bugs. However, this does find real bugs in the code, and formalizing code and specs require people to think deeply and formally on aspects of the problem. It just doesn't prove the code to be correct, or even that it satisfies the actual spec.

afarrell 4y ago

> Airplanes crash...but nobody seems to care If you think that nobody cares when airplanes crash, that signals that you likely want to: 1. Re-evaluate the evidence. Boeing was fined $2.5 Billion[1] over the MCAS debacle after it was a major news story. 2. Talk to someone about burnout. Cynicism is one of its major symptoms[2]. [1] https://www.justice.gov/opa/pr/boeing-charged-737-max-fraud-conspiracy-and-agrees-pay-over-25-billion https://www.justice.gov/opa/pr/boeing-charged-737-max-fraud-... [2] https://alifeofproductivity.com/remember-burnout-and-cynicism-go-hand-in-hand/ https://alifeofproductivity.com/remember-burnout-and-cynicis...

astrange 4y ago

Airplane code certainly is put through “formal verification”, but also “putting it through formal verification” is not a magic spell that removes bugs from a program. It only proves it does what is in the spec. It seems like the word “formal” impresses people too much.

oldgradstudent 4y ago
> It only proves it does what is in the spec. Worse than that. Usually, it only proves that a simplified version of the code satisfies to some extent a translation of the spec to some formal language. And "prove" only means that some rather buggy tool printed "Valid". Every point in this chain can and often does introduces bugs. However, this does find real bugs in the code, and formalizing code and specs require people to think deeply and formally on aspects of the problem. It just doesn't prove the code to be correct, or even that it satisfies the actual spec.