Even then you don't know if program is correct. There have been pieces of software running in production for 20 or 30 only to fail because of some unforeseen and planned for error condition.
My favorite was the Comair christmas failure back in 2004 or 2005. I tried googling the root cause, but I think it was an Integer overflow in the 16 bit integer they used for storing the flight number. The system was designed in the mid 80s and 65535 flights was an insane amount, but but when the software failed on Christmas it interupted more than 1,100 flights.
I am curious why people are downvoting me. It seems obvious to me to that proving software is correct is hard or impossible. It building and passing the tests help to increase confidence in correctness, but doesn't prove it.
No one disagreed with this comment and it is one of the least controversial thing I have said on HN. I think I have a downvote fairy, someone who just downvotes everything I say. If so, why bother? If I don't have one then when you downvoted me, why didn't you respond?
I disagree. For instance, if I'm writing something in C and I know that it is syntactically and semantically correct, I know that it will definitely compile.
Go hijacks control flow and makes it more difficult to reason about how your code will be compiled and executed. At least that is true in my personal experience.
Sorry, I don't understand what you mean by "Go hijacks control flow". Could you elaborate cases, where Go did not behave as you expected? And where syntactic and semantic correct Go code did not compile?
As far as my understanding is concerned, channels are a way for goroutines to pass data between one another, correct? Yet in this particular case, the channel `messages` is operating in the same manner as a generator or array. So, am I creating goroutines by passing messages to the channel or am I just using the channel as a simple buffer?
Channels are a safe way for goroutines to communicate. Safe here means, that the channel itself performs all the necessary locking needed for any number of goroutines to read or write "at the same time" to and from the channel. Other than that it does behave like a plain pipe. You write into it and can read from it "on the other side". Creating a channel does not create a goroutine. A goroutine is only created if you use the "go" command, like "go f(42)". This would run the evaluation of f(42) in a separate goroutine, which behaves like a thread, but uses less resources. So in neither of your examples, goroutines are created. You can optionally add buffering to the channel. A write to a channel without a buffer blocks, until the value you write to the channel is read. If you have buffers, you can fill them without blocking, even if the values are not consumed immediately. Without the buffer, the first example would get stuck, as the first write to "messages" would block until there is a read on that channel - which is never performed. But due to the buffering, the two writes to "messages" are performed without blocking, and the values can be read after that. A third read on the then empty channel would also block infinitely.
The flow of data through channels can be confusing until the concept becomes familiar, but the behavior is well-defined, so the behavior is as easy or difficult to predict as of any program of the given complexity.
It really just seems like you're saying "When I think my Go code is correct, it turns out it often isn't, but when I think my ${other_programming_language_i_know_better} code is correct, it turns out it usually is.
When I read about channels and various forms of IPC/inter-thread communication in most other languages, and remember the past pain of threads and mutexes in C/C++, I am so happy to be able to send a message in Erlang to another Erlang process (Pid) as easily as this:
Pid ! {self(), 42}
And in the process identified by Pid, to receive the message:
receive
{From, Data} when is_pid(From) ->
handle_data(From, Data)
end
And beyond that, the process identified by Pid can be running on a physically separate host system - it's transparent.
Too bad we can't use Erlang for systems programming, but you can't have everything!
>Am I implicitly creating goroutines by using channels or am I simply creating a buffer?
A channel is just a thread-safe queue. An unbuffered channel blocks until something else receives the sent value. A buffered channel allows n sends until it blocks. Using a channel will never create a new goroutine, its just a way send data. You can use a select statment to wait on sending or reciving from multiple channels or to send or get without being blocked by a full or empty channel.
In C you could put together a RW mutex, condition and a linked list or array and have the same thing pretty much.... If you want to create a goroutine you need to invoke "go X".
My favorite was the Comair christmas failure back in 2004 or 2005. I tried googling the root cause, but I think it was an Integer overflow in the 16 bit integer they used for storing the flight number. The system was designed in the mid 80s and 65535 flights was an insane amount, but but when the software failed on Christmas it interupted more than 1,100 flights.