Here’s the intuition that’s making me doubt the utility of provably correct system design to avoiding bridge crashes:
I model the process leading up to a ship that doesn’t crash into a bridge as having many steps.
1. Marine engineers produce a design for a safe ship 2. Management signs off on the design without cutting essential safety features 3. Shipwrights build it to spec without cutting any essential corners 4. The ship operator understands and follows the operations and maintenance manuals, without cutting any essential corners 5. Nothing out-of-distribution happens over the lifetime of the ship.
And to have a world where no bridges are taken out by cargo ships, repeat that 60,000 times.
It seems to me that provably safe design can help with step 1--but it’s not clear to me that step 1 is where the fault happened with the Francis Scott Key bridge. Engineers can and do make bridge-destroying mistakes (I grew up less than 50 miles from the Tacoma Narrows bridge), but that feels rare to me compared to problems in the other steps: management does cut corners, builders do slip up, and O&M manuals do get ignored.
With verifiable probabilities of catastrophe, maybe a combination of regulation and insurance could incentivize makers and operators of ships to operate safely—but insurers already employ actuaries to estimate the probability of catastrophe, and it’s not clear to me that the premiums charged to the MV Dali were incorrect. As for the Francis Scott Key, I don’t know how insuring a bridge works, but I believe most of the same steps and problems apply.
(Addendum: The new Doubly-Efficient Debate paper on Google’s latest LW post might make all of these messy principal-agent human-corrigibility type problems much more tractable to proofs? Looks promising.)
I totally agree in today’s world! Today, we have management protocols which are aimed at requiring testing and record keeping to ensure that boats and ships in the state we would like them to be. But these rules are subject to corruption and malfeasance (such as the 420 Boeing jets which incorporated defective parts and yet which are currently flying with passengers: https://doctorow.medium.com/https-pluralistic-net-2024-05-01-boeing-boeing-mrsa-2d9ba398bd54 )
In that world, we can implement provable formal rules governing every system, from raw materials, to manufacture, to supply chain, to operations, and to maintenance.
In an AI world, much more sophisticated malfeasance can occur. Formal models of domains with proofs of adherence to rules and protection against adversaries is the only way to ensure our systems are safe and effective.
Here’s the intuition that’s making me doubt the utility of provably correct system design to avoiding bridge crashes:
I model the process leading up to a ship that doesn’t crash into a bridge as having many steps.
1. Marine engineers produce a design for a safe ship
2. Management signs off on the design without cutting essential safety features
3. Shipwrights build it to spec without cutting any essential corners
4. The ship operator understands and follows the operations and maintenance manuals, without cutting any essential corners
5. Nothing out-of-distribution happens over the lifetime of the ship.
And to have a world where no bridges are taken out by cargo ships, repeat that 60,000 times.
It seems to me that provably safe design can help with step 1--but it’s not clear to me that step 1 is where the fault happened with the Francis Scott Key bridge. Engineers can and do make bridge-destroying mistakes (I grew up less than 50 miles from the Tacoma Narrows bridge), but that feels rare to me compared to problems in the other steps: management does cut corners, builders do slip up, and O&M manuals do get ignored.
With verifiable probabilities of catastrophe, maybe a combination of regulation and insurance could incentivize makers and operators of ships to operate safely—but insurers already employ actuaries to estimate the probability of catastrophe, and it’s not clear to me that the premiums charged to the MV Dali were incorrect. As for the Francis Scott Key, I don’t know how insuring a bridge works, but I believe most of the same steps and problems apply.
(Addendum: The new Doubly-Efficient Debate paper on Google’s latest LW post might make all of these messy principal-agent human-corrigibility type problems much more tractable to proofs? Looks promising.)
I totally agree in today’s world! Today, we have management protocols which are aimed at requiring testing and record keeping to ensure that boats and ships in the state we would like them to be. But these rules are subject to corruption and malfeasance (such as the 420 Boeing jets which incorporated defective parts and yet which are currently flying with passengers: https://doctorow.medium.com/https-pluralistic-net-2024-05-01-boeing-boeing-mrsa-2d9ba398bd54 )
But it appears we are rapidly moving to a world in which much of the physical labor will be done by robots and in which each physical system will have a corresponding “digital twin” (eg. https://www.nvidia.com/en-us/omniverse/solutions/digital-twins/ ).
In that world, we can implement provable formal rules governing every system, from raw materials, to manufacture, to supply chain, to operations, and to maintenance.
In an AI world, much more sophisticated malfeasance can occur. Formal models of domains with proofs of adherence to rules and protection against adversaries is the only way to ensure our systems are safe and effective.