Tony Morris

This is false. Software is not write-only. Software requires maintenance. Code need to be readable. It's primary audience is humans.

furthermore, how can we have any confidence that the computer is doing what we want if we cannot reason about the program?

We run it and see if it gives the answer and/or behaviour we want with the data we gave it. Same way people use spreadsheets.

Honest question: how do you know if the answer/behaviour observed is the answer/behaviour you want?

When it's the same outcome as what you would have got doing it by hand, and when your spot checks look right.

When we formalise those spot checks, we give them names like unit tests, acceptance tests, and test vectors :)

I hope Boeing "spot-checked" all the possible combinations of inputs in their avionics system on the 737-800 I was flying on last night :)

Yep, Boeing knows how to write & test safety critical software: https://en.wikipedia.org/wiki/Safety-critical_system#Software_engineering_for_safety-critical_systems …