This is a slightly above my pay grade, so take it with a bit salt.
Type systems in general reject some programs as invalid, but this claim is usually made with powerful type systems in mind; think Haskell, Idris, Rust. I only played with these casually, but it is true that you can write some code, and then let yourself be guided by compiler in fixing all the errors. It's often the case that the resulting program just works.
Rust's borrow checker is a part of its type system, based on some flavor of linear types if I remember correctly. Think about it: the type system can protect you from double frees. This is powerful.
In Haskell, for starters, you can't do any side effects outside of IO monad. You can express precisely what a given function is allowed to do.
In dependently-typed languages you can express that, for example, a function concatenating lists of length n and m returns a list of length n + m.
And aside from these above there is a lot of other, less magical things: no nulls, exhaustiveness checks for ADTs, some focus on immutability, lack of exceptions, and so on.
Now, I doubt we are all going to write Idris in five years, and even there bugs do happen obviously. But the idea compiles==works is not entirely out of this world.
Type systems in general reject some programs as invalid, but this claim is usually made with powerful type systems in mind; think Haskell, Idris, Rust. I only played with these casually, but it is true that you can write some code, and then let yourself be guided by compiler in fixing all the errors. It's often the case that the resulting program just works.
Rust's borrow checker is a part of its type system, based on some flavor of linear types if I remember correctly. Think about it: the type system can protect you from double frees. This is powerful.
In Haskell, for starters, you can't do any side effects outside of IO monad. You can express precisely what a given function is allowed to do.
In dependently-typed languages you can express that, for example, a function concatenating lists of length n and m returns a list of length n + m.
And aside from these above there is a lot of other, less magical things: no nulls, exhaustiveness checks for ADTs, some focus on immutability, lack of exceptions, and so on.
Now, I doubt we are all going to write Idris in five years, and even there bugs do happen obviously. But the idea compiles==works is not entirely out of this world.