What? I get myself in the mood for manual tests too.
We're not talking past each other. You can't just quote "testing" and embed extra meaning into that after the fact. There's no way I would know what you're talking about.
>I'm not a python + mypy regular user though, so I don't know where it's limits are, but particularly with the haskell comparison, it does not support GADTs (https://github.com/python/mypy/issues/8252). Also, I know it doesn't support Rust's affine type system (ownership/borrows).
Nah when it comes to the lang extensions almost nothing comes close. I'm just talking about regular haskell ADTs.
The affine stuff isn't relevant as python uses a GC. What does it even mean to do borrow checking when nothing owns a variable in python?
It's quite obvious I'm just referring to the ADTs here.
Python supports regular ADTs better than typescript. So it's better imo. But that's just my initial opinion, I don't use ts extensively so it might be better.
>I personally believe NodeJS is the best of the "scripting" languages, but that's a whole 'nother discussion.
If You mean JS. then no, JS is horrible. Typescript has an argument here, I think that's what you mean.
>I agree on being flexible, I like using Haskell/Rust because of this as well. I certainly disagree that python matches any of those others in type level power though.
It matches it in terms of ADTs and where relevant.
>Theorem proving != engineering, and this is why Haskell/Idris/ML languages at large never hit mainstream properly. If you try to write the kind of types that could even attempt to get correctness absolutely right, less than 0.1% of programmers would be able to use or work on your codebase.
So? I never made this claim. I just said there are other methodologies to employ other then strict fanatical loyalty to testing. I simply used Idris as an example of an alternate path. In fact I specifically STATED that it would be hard to use proofs with Idris.
>I don't think TLA+ is relevant here because it's mostly used for testing distributed/concurrent systems in practice, and is not a PL so-to-speak.
The point was using proof to write correct programs. So it's completely relevant as TLA+ is used for that.
>Naturals (& peano numbers) are the categorical example of dependent types that are useful -- in Haskell, natural numbers are the set of positive integers including zero. It makes the -1 case impossible (i.e. fail to parse @ the program boundary), which is the point.
ah my mistake I had a brain fart and thought you were referring to Haskells Num or something along those lines. Yes if by Nat you mean Haskell Nat or unsigned int, then that makes sense.
>I think we're agreeing, but you just said two very different things -- most things (especially important ones) cannot be easily solved at the type level.
I never said two different things. I think you just made some assumptions and responded to some paragraphs without reading far enough. Like your "Theorem proving != engineering," comment. If you read further you'd realize I already know about what you're saying.
My overall point on this front is aspects of proving can help type checking and FP and other techniques reduce error rate by a large margin.
>How do you type-check a redis connection at compile time? or a database like postgres at runtime? You can't, really -- because they are inherently dynamic things.
I'm not sure why you're telling me this. Did I make a claim that type checking can work on a redis connection?
Do you remember when I said integration tests are more important then unit tests? And unit tests are mostly practically trivial? Well type checking is sort of involved with that. I mean these are points I've been making throughout our conversation suddenly your like "How do you type check a redis connection?" as if I haven't made any of those points. I made a point and you made the same point.
Anyway we agree here.
>Yeah this is where we disagree -- I think this case called for it, you disagree.
Yes. To get into more detail here. The point is the infra cost of integration tests we disagree on that, I don't think it's worth it all the time I think you believe it's worth it in more cases.
For the take home project I still don't think it's worth it. But I concede I'm wrong because the Reviewer is looking for tests and I need to cater to what the reviewer is looking for.
>We agree that sometimes tests are not necessary or warranted.
Well you told me you have testing enshrined. So I was disagreeing with that. I think you were just making a statement about the importance of testing. In actuality we're more in agreement about the nuance of testing.
>No problem, always glad to have a debate, and being able to have them on HN is why I still come to this site!
Sometimes these conversations generate some heat on HN. I actually don't mind the heat, keeps people brutally honest.
Great talking to you as well!