Except Ada has UB (they used to call them bounded errors, but the semantics are basically identical), and reading the musings of ADAists[0]
> I would say, having looked at hundreds of thousands of lines of Ada, that I have had a disappointingly frequent experience in finding the UNCHECKED_CONVERSION generic used in production Ada code.
> I agree that this is often a mark of poor craftsmanship and
unhesitatingly discourage its use, but it is there
If finding potential UB in Ada programs is as simple as grepping for unchecked_conversion, then that's a big step forward compared to C, don't you think?
The claim is that it's impossible to avoid UB in real world C, but not impossible in real world $SAFERLANGUAGE, with Ada as an example. Any language that allows you to poke around in memory (a feature you need for embedded systems) will contain unsafe constructs. The question is whether you can tell by looking whether a particular piece of code is safe or not.
> I would say, having looked at hundreds of thousands of lines of Ada, that I have had a disappointingly frequent experience in finding the UNCHECKED_CONVERSION generic used in production Ada code.
> I agree that this is often a mark of poor craftsmanship and unhesitatingly discourage its use, but it is there
[0] https://www.cs.york.ac.uk/hise/safety-critical-archive/2011/...