Hacker News new | ask | show | jobs
by first_amendment 3217 days ago
> I just don't think that we have sufficient evidence to conclude that using type systems to aid the development of concurrent code actually leads to better concurrent code.

This is like saying we don't have evidence that evolution is real.

Type systems are proof systems. If a type system encodes concurrency safety, and a program is valid under that system, then you can be 100% certain that program doesn't have a race condition bug due to shared state between threads.

If a type system can prove buggy concurrent code is invalid code, then by definition it leads to better valid concurrent code.

1 comments

Lol! You would not be successful as a scientist with this attitude.

A type system is a proof. But the proof in the type system is not a proof that it’s better to use a type system than not. That’s an entirely separate question.

I think that type systems are good at some things. Concurrency isn’t one of them.

I made an argument. What's yours? You just made a statement of opinion without any justification.

Additionally your opinion is wrong, by simple counter example. Rust's type checker already has the ability to prevent data races: https://blog.rust-lang.org/2015/04/10/Fearless-Concurrency.h... This works today.