Can a programming language be written that makes it impossible to write invalid code and be expressive?

[Ike]

Coding is logic and within logic there are valid and invalid ways 
combine smaller code blocks.

When we code as programmers we are forming `functions` that take 
inputs and create outputs no matter how complex or simple the 
code is.

There are only 2 ways that code can become invalid as far as 
programmers are concerned: 1. The wrong inputs 2. Combining the 
inputs in an invalid way.

If we design a function that is logically sound for specific 
inputs and unsound for other inputs then the program will be 
unsound for some specific inputs and hence the program, to be 
sound, must be driven in such a way never to produce inputs in to 
the function that is invalid.

If we design a function that is logically unsound then it is 
essentially a "programming logic error".

It seems that any programming language should have these 
foundations covered as the root so that all programs written in 
it are valid. Programs so far only seem to deal with extreme 
logic errors.... basically they handle only extremely unsound 
programs that produce invalid machine code but otherwise will 
function unsoundly if they pass the machine test. E.g., dmd will 
produce a valid executable that can run and then immediately 
crash. It is the most basic level of writing sound programs, it 
covers the extreme errors but it does little more to help.


Are there languages that prevent all systematic programming 
errors(not errors in choice but fundamental errors that will lead 
causatively lead to unsound programs)?

There are mathematical programming languages like COQ that is 
sort of like an ideal programming language in that any valid 
program will function with absolute certainty in the result. Pure 
languages also sort of work along these lines as as they do focus 
on the input's more by restricting the inputs to be well 
localized.

Are there any languages, that effectively can pretend all 
programming logic errors. It will be able to catch all errors by 
making sure all inputs correct and the function logic is correct? 
  Obviously covering the space of all possibilities is probably 
impossible but we should be able to write programs today with 
reasonable assurance that the program will function as intended. 
A lot of programming now days is involved in making sure a 
program will function correctly most of the time. We validate 
arguments(e.g., simple null checks), we have contracts, etc...


It seems that maybe this is not the way to program. We have to do 
a lot of work that a compiler could do for us. It knows what is 
valid(it's in the math) and it has the power(cycles) to check 
things very thoroughly. People seem to act like things such as 
flow analysis are evil because it is complex... yet that is 
precisely what the compiler needs to do... it is even more 
complex for the programmer to do it... and if it's done in the 
compiler it benefits all programmers so the leverage gained in 
creating more efficient and competent programmers grows.

The input to most programs is actually quite well defined: Some 
keyboard entry here, a mouse click there, a file being read here, 
etc... It's not like we are shoving random input's in to the 
program. In fact, most humans can generally provide the input 
that a program wants well and standardizations in interface and 
program design have helped with this.

I feel that even with all the meta programming and fancy features 
I'm still programming punch cards. Rather than working with very 
high level abstractions most of the time I still have to deal 
with very basic low level issues constantly. There always seems 
to be a trade for speed in this case but I'm not convinced that 
high level abstractions have to be slower, in fact, they could be 
faster due to optimizations that cannot take place otherwise.

It seems it is a hard problem since one wants the right 
abstractions at all times and using the wrong abstractions can 
really cause major issues throughout the program.

But the language, compiler, an IDE should all be on my side in 
making my job as easy as possible with the most benefit... I 
shouldn't have to fight them ever... yet I believe I spend more 
time trying to figure things out, fix things, optimize things, 
etc than I do actually doing the real structural programming that 
I wanted to do in the first place.

E.g., if I want to write a program I should just be able to write 
it and optimize all my time in to doing what is necessary to 
actually get the program done... rather than spending the 
majority of time doing other things completely unrelated to the 
actual task of programming(which is the task of "modern" 
programming it seems).

I guess we just haven't arrived at this programmers utopia yet?