[de_keyboard]

Will we care about proofs and type-systems once we have AI systems that reliably answer questions like "does this code do X?" and "under what conditions does this code violate invariant Y?"