>I won't say any more on the subject. Yeah don't bother. >We're not considering language extensions (which are built in BTW, on par with using the stdlib), bu

>I won't say any more on the subject. Yeah don't bother. >We're not considering language extensions (which are built in BTW, on par with using the stdlib), but we're considering completely separate ecosystem plugins that do type checking? Nonsense. It's not nonsense, the language extensions should not be included because the functionality in Haskell is so far and above what ANY type checker typically does. Clearly. You're being utterly too pedantic here. When I say python types match haskell in power I am obviously not touching upon GADT or RankN. You're getting into the weeds. It has nothing to do with extensions being "on par with stdlib" >Tracking usage of variables is useful, whether you use GC or not -- it's a matter of ability in the type system. My point is that you cannot specify in your code that a value should be used "at most once", which is what affine types afford you. Yeah but not strictly necessary for python which has a GC, but strictly necessary for Rust which has ownership. >I will not say more on this Yeah don't bother. Sort of rude. But whatever. >No, I mean JS, and in particular NodeJS as an execution platform, because it has no GIL, can do threads, async io is a first class concept, were flexible enough to get used to transpilation (which lets something like Typescript exist). It can't do threads. I just looked it up. Worker Threads are processes that use some form of IPC. Literally a whole new v8 engine. I was right. Also JS is a horrible language. It's crazy you use haskell and you're ok with things like undefined which basically is a nonsense instance that can flow from one end of your code to another. >The type is called Natural, and I wrote Natural. Nope the type is called Nat. https://hackage.haskell.org/package/fin-0.3/docs/Data-Type-Nat.html https://hackage.haskell.org/package/fin-0.3/docs/Data-Type-N... and in Idris: https://www.idris-lang.org/docs/current/base_doc/docs/Prelude.Nat.html#Prelude.Nat.Nat https://www.idris-lang.org/docs/current/base_doc/docs/Prelud.... But this has nothing to do with anything does it? I thought you were referring to a more general type Num. >You said that it can prove a system to be "correct". Unfortunately I can't know what you meant by "correct", but the type system will not help you with many of the practical issues that are most important when writing code. And I wrote extensively on what that means and you read it so you know what I'm talking about. There's no need to get pedantic and argue on pedantic points that are obviously contrary to the obvious meaning of what I'm saying. >That's where good engineering comes in. Yep, but do you have a point? Why make this statement? >This will be my last on this discussion, was good! I don't think you think it was good. I think you're annoyed. That's why you want to cut it off.