3 ms·
It feels like the author is describing a healthy type system and language purity. In most programming languages, the pain points they describe are real - how d
by johnday 5y ago
It feels like the author is describing a healthy type system and language purity.
In most programming languages, the pain points they describe are real - how do we know that a program will give back exactly what we put in?
The answer is to provide it with an appropriately restrictive type such that any output is necessarily of the right shape. Types allow us to do this exact kind of "offloading", so that we simply trust the compiler to know when we are plumbing things together correctly.
Language purity is really helpful with trusting that a piece of code does what it says it does, and nothing else. If our language is impure then the scope of any given function is essentially unbounded. With purity, it can only perform computations based on the things that are locally available to it, and that severely bounds the amount of leeway a programmer has in its implementation - and hence the number of ways things can go wrong.
In short, an effective, ergonomic, statically-typed programming language can solve most or all of the author's woes. I hope they find one that fits their needs.
- kubb 5y agoIt sounds to me like the author wants to see how their code behaves on certain inputs instead of predicting its correctness mentally. Current static type systems don't solve this. There are proof assistants, but limited to academia. For a concrete (and possibly oversimplified) counterexample, try to use your favorite static type system to verify that a function returns the n-th prime.
- plutonorm 5y agoThere is a difference between the shape of a thing and the specific instance of the thing. To explore the operation of code at an edge case you need to create an instance of the thing that represents that edge case.