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

[Ike]

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
"