About the last part of the post, Ada has asserts if my memory is correct. And Oberon, if it's still alive. And Eiffel with assertions on preconditions and postconditions of routines (functions or procedures.) Probably those features were shared by many other languages that were fashionable some 30 years ago and never became mainstream. Then Java and C++ did to the industry what C did in the 70s/80s and all those features retreated from what developers almost used to what researchers wrote in their papers.