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?

On Sunday, 28 July 2019 at 04:58:40 UTC, Ike wrote:
> It seems that any programming language should have these foundations covered as the root so that all programs written in it are valid.

Depends on your definition of valid, but I believe solving this would require solving the "Halting problem" (https://en.wikipedia.org/wiki/Halting_problem) which is unsolvable on Turing machines.

On Sunday, 28 July 2019 at 04:58:40 UTC, Ike wrote:
> 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.

Do you mean purely functional languages? You certainly can get runtime-issues in those, like infinite recursion. Also, the execution matters, if you get you have "f(x) AND g(x)" where f(x) enters infinite recursion and g(x) resolves to false, then the program can complete if g(x) is resolved first, or if both f(x) and g(x) are resolved concurrently and the runtime system is able to abort the execution of f(x).

Anyway, the key point of the halting problem is that this situation cannot be avoided unless you restrict the space of problems that can be solved.

https://en.wikipedia.org/wiki/Halting_problem

On Sunday, 28 July 2019 at 07:30:02 UTC, Ola Fosheim Grøstad wrote:
>
> Anyway, the key point of the halting problem is that this situation cannot be avoided unless you restrict the space of problems that can be solved.

Of course, in theory it is still possible since we always can put an upper limit on the amount of memory, time, input.

But it is not something we can expect to be resolved in our lifetime.

On Sunday, 28 July 2019 at 04:58:40 UTC, Ike wrote:
> Coding is logic and within logic there are valid and invalid ways combine smaller code blocks.
>
> [...]

Have a look at Idris and F*.

On Sunday, 28 July 2019 at 04:58:40 UTC, Ike wrote:
>
> I guess we just haven't arrived at this programmers utopia yet?

Could we have a programming language that writes its own programs, so that no more programmers are needed? In theory maybe; but someone will have to write it :)

On Sunday, 28 July 2019 at 09:09:37 UTC, XavierAP wrote:
> On Sunday, 28 July 2019 at 04:58:40 UTC, Ike wrote:
>>
>> I guess we just haven't arrived at this programmers utopia yet?
>
> Could we have a programming language that writes its own programs, so that no more programmers are needed? In theory maybe; but someone will have to write it :)

This was done in 1980 🙂

https://teblog.typepad.com/david_tebbutt/2007/07/the-last-one-pe.html

On Sunday, 28 July 2019 at 09:09:16 UTC, Paulo Pinto wrote:
> On Sunday, 28 July 2019 at 04:58:40 UTC, Ike wrote:
>> Coding is logic and within logic there are valid and invalid ways combine smaller code blocks.
>>
>> [...]
>
> Have a look at Idris and F*.

Thanks, these are interesting and look like they are trying to head in the right direction.

"F* (pronounced F star) is a general-purpose functional programming language with effects aimed at program verification. It puts together the automation of an SMT-backed deductive verification tool with the expressive power of a proof assistant based on dependent types. After verification, F* programs can be extracted to efficient OCaml, F#, C, WASM, or ASM code. This enables verifying the functional correctness and security of realistic applications."

"Idris is a general purpose pure functional programming language with dependent types. Dependent types allow types to be predicated on values, meaning that some aspects of a program’s behaviour can be specified precisely in the type. It is compiled, with eager evaluation. Its features are influenced by Haskell and ML, and include:

    Full dependent types with dependent pattern matching
    Compiler-supported interactive editing: the compiler helps you write code using the types
    Type-driven overloading resolution
    Cumulative universes
    Totality checking
"