www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - Can a programming language be written that makes it impossible to

reply Ike <Ike.Turner gmail.com> writes:
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?
Jul 27 2019
next sibling parent JN <666total wp.pl> writes:
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.
Jul 28 2019
prev sibling next sibling parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
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
Jul 28 2019
parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
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.
Jul 28 2019
prev sibling next sibling parent reply Paulo Pinto <pjmlp progtools.org> writes:
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*.
Jul 28 2019
parent Ike <Ike.Turner gmail.com> writes:
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 

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
"
Jul 30 2019
prev sibling parent reply XavierAP <n3minis-git yahoo.es> writes:
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 :)
Jul 28 2019
parent Abdulhaq <alynch4047 gmail.com> writes:
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
Jul 28 2019