How the Boeing 737 Max disaster looks to a software Developer

Re:How the Boeing 737 Max disaster looks to a software Devel... by zestyping on Thursday April 18, 2019 @07:05PM (#19695558)

If the proof is more complex than the software, I don't see how that gains you anything. It's harder to verify that you've proved the right thing than to verify the software itself, so how does that help?

[ Parent | on HN ]

Re:How the Boeing 737 Max disaster looks to a software Devel... by crimsonalucard on Tuesday April 23, 2019 @12:04PM (#19729908)

In a type checked language. Your software is guaranteed to have no type errors. How hard was that?

[ Parent | on HN ]

Re:How the Boeing 737 Max disaster looks to a software Devel... by zestyping on Tuesday April 23, 2019 @03:35PM (#19732074)

That's a great example! It illustrates the point in a better way than I tried to.

A necessary part of why types are so useful is that understanding the types is easier than understanding the code itself.

If the types become so complex that they start to get harder to understand than reading your code (e.g. C++ template errors can sometimes get this bad), then they are no longer helpful.

[ Parent | on HN ]