You make a valid point: I used the word "bug" here without trying first to define it, and that led to confusion in my mind, and thus in my comment.

In that comment, I used the example of programs performing an ascending sort or a descending one. While both programs would be valid, one of them, at least, would not correspond to the intent of the programmer. From an engineering perspective, that would be considered a bug.

I guess an informal yet hopefully apt definition of the word bug could be "an error in the source code of a program leading to an incorrect behaviour of that program at runtime". That incorrect behaviour can take many forms: the most obvious one is the program breaking in the middle of a computation, without providing any result (a semantic bug). A second one is when the compiler will not accept the program as valid (a syntactic bug). A third one is the program producing the wrong result, as in my example (also a semantic bug).

In my mind, I only considered the first 2 kinds of errors as bugs, and qualified the last as something else, perhaps for the reason that only the programmer may really know the intent behind a program's implementation.

One of the goals when designing a programming language is to help reduce the occurrence of bugs. The main strategy is to turn bugs of the first kind (semantic) into bugs of the second kind (syntactic), or at least that is my understanding.

Concretely, with a powerful enough type system, one may express expected properties of a program using the provided syntax, and let the compiler validate these claims using only formal rules.

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.

Thank you, that's exactly what I had in mind when speaking about strongly typed languages. I don't think I could have presented it in a better way.