This guy is doing an excellent job illustrating why our programming languages are not good for configuration.

The thing is if you create the ultimate configuration language then you’ve also created the best possible programming language.

A computer has a finite amount of configurations and if you can create a programming language whose space of possible programs (post-compilation let’s say) maps faithfully to the space of possible configurations of the computer then you should be incapable of having a runtime error.

Now that you have this great configuration language you would want to use it to write as much of your logic as possible… If there is a computation that it can’t describe but the computer can perform then you’d write that computation as neatly and independently as possible, prove properties about it and then wrap it in your nice configuration language.

Suggesting that configuration should be handled by the type system is again a very good insight. We want configuration to terminate so that the program can start and a type system is there to “configure” your computation.

The type system is actually better illustrated as a theorem prover in my opinion, it allows you to prove that values of incorrect types wont be put in places they shouldn’t be in and once it gets to be sufficiently advanced then the types can have constraints to the point of almost being values. Which allows the system to make very strong guarantees about your computation.

Some examples from the real world of people converging on this goal:
Rust with unsafe fits the picture I just painted. Dhall wants to be the configuration language for systems programming. Statebox wants to be the language for everything, Lean has a similar goal but more traditional approach. Idris came to be as a Haskell where you can do most of your things in Agda, Haskell got jealous and now we’ll have dependent Haskell in a couple of years, Agda has the delay monad…

So basically, we already know where we want to go, currently I think Statebox is doing the most interesting work on making this a reality.

This guy is doing an excellent job illustrating why our programming languages are not good for configuration.

The thing is if you create the ultimate configuration language then you’ve also created the best possible programming language.

A computer has a finite amount of configurations and if you can create a programming language whose space of possible programs (post-compilation let’s say) maps faithfully to the space of possible configurations of the computer then you should be incapable of having a runtime error.

Now that you have this great configuration language you would want to use it to write as much of your logic as possible… If there is a computation that it can’t describe but the computer can perform then you’d write that computation as neatly and independently as possible, prove properties about it and then wrap it in your nice configuration language.

Suggesting that configuration should be handled by the type system is again a very good insight. We want configuration to terminate so that the program can start and a type system is there to “configure” your computation.

The type system is actually better illustrated as a theorem prover in my opinion, it allows you to prove that values of incorrect types wont be put in places they shouldn’t be in and once it gets to be sufficiently advanced then the types can have constraints to the point of almost being values. Which allows the system to make very strong guarantees about your computation.

Some examples from the real world of people converging on this goal: Rust with unsafe fits the picture I just painted. Dhall wants to be the configuration language for systems programming. Statebox wants to be the language for everything, Lean has a similar goal but more traditional approach. Idris came to be as a Haskell where you can do most of your things in Agda, Haskell got jealous and now we’ll have dependent Haskell in a couple of years, Agda has the delay monad…

So basically, we already know where we want to go, currently I think Statebox is doing the most interesting work on making this a reality.