News for hackers. Stuff that matters.
Re:A Flexible Type System for Fearless Concurrency by fweimer on Sunday May 14, 2023 @05:47AM (#35936734)
These papers typically contain (semi-)formal descriptions of the type system and various proofs about it. The technical material for this paper is in an appendix:

https://www.cs.cornell.edu/andru/papers/gallifrey-types/appe...

For real-world languages, this is even more involved, and existing formalizations only cover supposedly distinct sub-languages, not the full language (with the risk being that there are unexpected interactions). Most languages also have complicated things like higher-order functions or some form of polymorphism, and the new type system would have to be integrated with that.

Re:A Flexible Type System for Fearless Concurrency by mafribe on Sunday May 14, 2023 @08:23AM (#35937441)
This is true, but higher-order functions and polymorphism are extremely well-understood. (Including that there are various compromises with type-inference when you combine them with other constructs),
Re:A Flexible Type System for Fearless Concurrency by di4na on Sunday May 14, 2023 @08:47AM (#35937553)
No. No they really are not well understood and the complications in the type system multiply fast.