> But until the halting problem is solved at a compiler level (at a level that can account for runtime cases) Idris can already check for totality (i.e. guaran

> But until the halting problem is solved at a compiler level (at a level that can account for runtime cases) Idris can already check for totality (i.e. guarantee its programs will halt) without solving the (unsolvable) halting problem. So we're almost there! And even in Haskell, you can write certain classes of concurrent code without thinking thanks to 1) its great RTS and concurrency libraries and 2) the fact that Haskell programs compose so well: If I have thread safe programs A and B, Haskell gives me a variety of ways to compose their results in such a way that thread safety is always preserved.