Despite enjoying the terseness of C, with curly braces and short notations, many "normalized" things in C used to trip up math students I would tutor in element

Despite enjoying the terseness of C, with curly braces and short notations, many "normalized" things in C used to trip up math students I would tutor in elementary programming classes. "Why is `=` assignment and not `==`? How can a function not produce a value? Why does `||` mean "or"?, etc. Pascal family languages usually end up much more long winded, but can often be more easily explained to non-programmers than C solutions. I spent a couple years doing down the Ada rabbit hole in open source and was amazed how many elements of the problem domain you express directly with the language, and how you can constrain your program to catch domain-specific issues with the compiler. With the rise of things like ChatGPT, I'm curious if the next revolution for programming languages is focusing on constraints to verify correctness rather than expression of what to do. This might help help an AI model develop code and provide validity checks on the generated solution.