5 ms·

> No this bug wouldn't have been caught. I'd have to write the test for it. ... Ah OK, so this is where I think that we're talking past each other. When I say

> No this bug wouldn't have been caught. I'd have to write the test for it. ... Ah OK, so this is where I think that we're talking past each other. When I say "testing", and the reason I focus on making them automated is that when I sit down to write tests, if I'm really up to it I get myself in a mood where I'm thinking of what can go wrong. Doing that is what I'm suggesting might have made the difference. > This is where you are wrong. Python has what I call an opt-in type system meaning it's optional and it can be as strong as you want it to be. You choose the external type checker like mypy and those type checkers can be as powerful as you want. ... > > The python type system can even do Haskell/Rust level exhaustive matching on sum types: https://tech.preferred.jp/en/blog/python-exhaustive-union-ma https://tech.preferred.jp/en/blog/python-exhaustive-union-ma... > So this comes back to me not writing much python -- but I have used typing + mypy briefly a while ago, but I'd need to see some claims it is nowhere near as powerful as Typescript/Rust/Haskell. 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 https://github.com/python/mypy/issues/8252). Also, I know it doesn't support Rust's affine type system (ownership/borrows). It's true that mypy could in theory do this, but it does not, and I do not expect it to anytime soon (backing for the other projects is more sound anyway). I personally believe NodeJS is the best of the "scripting" languages, but that's a whole 'nother discussion. > So modern python matches these language in type level power, it's just optional so it's not as pervasive as typescript but the option is there and when utilized it's equal if not better in power. But proof based coding isn't solely just on using types to prove out your code. I just used idris as an example of an alternative path. The reality is Idris is a bit too extreme because coding those types takes too much effort. > > Basically i change my coding style to both minimize errors and allow me to build a minimal proof in my head. I use coding style, proofs in my head, and a strong/versatile type system all in conjunction to minimize error rate to low enough levels that tests are less important. 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. > You can't do integration tests without using infrastructure and spinning up processes. Let me put it to you plainly. It's not ME who thinks it's difficult. It's the majority of the developer population knows it's much more difficult then unit tests. That's why such a segregation even exists. The fact that we categorize the tests into integration tests and unit tests speaks to huge differences between the two in difficulty. > > You may think integration tests are easy, but that's just your own opinion. This is different from the overall general opinion which is more inline with what I'm saying. Regardless of what other devs thing of it, it's worth doing IMO. Here's the project I linked before https://testcontainers-python.readthedocs.io/en/latest/README.html https://testcontainers-python.readthedocs.io/en/latest/READM... > Dependent types are enough to prove a program is correct given a set of specifications. Of course not everything can be proven. But most things can. Disagree with this. For example, memory leaks. If I define "correct" to be "doesn't leak memory", Haskell (for example -- don't know what the memory is like in Idris) is going to have a hard time. There are things that are hard/impossible to encode into dependent types. > Theorem proving is the title. or aka proving anything mathematical or aka proving mathematical programs meet mathematical specs. Dependent typing is one way to go about this. There are other ways. The intended design of idris is similar to TLA+ the intention is to allow the user to prove the program correct to a spec and avoid unit tests via proof. 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. 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. > How is using a nat more safe than an int? A nat just makes it more general. https://hackage.haskell.org/package/natural-numbers-0.1.2.0/docs/Data-Natural.html#t:Natural https://hackage.haskell.org/package/natural-numbers-0.1.2.0/... 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. > With something like idris you can, technically speaking, eliminate the need for unit tests all together. But this is a technical thing. In practice it's really hard to achieve this due to how hard it is to write these proofs. But the technical level of safety is operating at the highest level here. 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. 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. Now in the case of unit tests, I'd argue that a good type system is one of the only things that can prevent you from having to write lots of unit tests. I'm pretty sure we agree on this! > I'll tell you this: I don't enshrine the concept of testing. It's always a case by case basis. Yeah this is where we disagree -- I think this case called for it, you disagree. We agree that sometimes tests are not necessary or warranted. > Hey I know this thread got a little heated. I want you know that I appreciate your viewpoints even though I disagree with a lot of points. I think heated but respectful debates are healthy and I definitely learned something here. Conversations where people are overly polite I feel like I learn nothing because people rather be polite then honest. So appreciate all the time you took to reply. I may be clashing hard against your points but there's nothing but respect here. You are clearly experienced. No problem, always glad to have a debate, and being able to have them on HN is why I still come to this site! We can disagree, and I benefit from learning where your disagreements are (I don't there are actually many, I think our stances on testing and types are very similar outside of me just not liking in python in any meaningful way).

formulathree 3y ago
>Ah OK, so this is where I think that we're talking past each other. When I say "testing", and the reason I focus on making them automated is that when I sit down to write tests, if I'm really up to it I get myself in a mood where I'm thinking of what can go wrong. >Doing that is what I'm suggesting might have made the difference. 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 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!

formulathree 3y ago

>Ah OK, so this is where I think that we're talking past each other. When I say "testing", and the reason I focus on making them automated is that when I sit down to write tests, if I'm really up to it I get myself in a mood where I'm thinking of what can go wrong. >Doing that is what I'm suggesting might have made the difference. 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 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!