3 ms·

I think GP's point was that most[1] programs that can be represented will fail to please the programmer or his principals. The act of programming is navigating

by User23 2y ago

I think GP's point was that most[1] programs that can be represented will fail to please the programmer or his principals. The act of programming is navigating the state space of all possible programs and somehow finding one that has the desired properties and also doesn't otherwise suck. When viewed through that lens, a type system preventing most programs from being represented is a good thing, since odds are every single program it prevents is one that is unpleasant or otherwise sucks. [1] of the countably infinite possible programs, virtually all

auggierose 2y ago
That would make sense if writing a program would be similar to randomly drawing a program from a pot of programs. If instead I have a good idea what I want to write, the type system may either guide me towards the solution, or hinder me. It usually hinders me, I don't need a type system to guide me, but I like a type system that can check for trivial errors (oh, I meant to pass a list of numbers, not just a single number).