You know every single error every framework function can call? Every single error in your entire code base? What about tomorrow when Bob changes some code? >

You know every single error every framework function can call? Every single error in your entire code base? What about tomorrow when Bob changes some code? > If function a calls function b, and function b throws errors x y and z, why is it I cannot check for x y and z in function a? How often do you have a single function in your call stack? Do you also handle/swallow every error in every function or do you propagate those errors? So function q throws errors it was called by function p that throws and by the time you get back to a the list is a lot longer than x, y, z. Formal verification is a red herring. I know my software either handles all the errors that it can or stops processing and informs someone. Error types don't remove complexity or make humans better at error handling.