> Basically: I need a Car Object with these exact fields vs give me a thing with the field "foobar" that contains something that I can concatenate with another things. Um, that's another matter entirely. Polymorphism.…
>If you argue that X is better than Y and Z because X is all you know, you just sound like a cultist. Learn first, argue later. Apparently, you didn't look in the mirror. Oh, well. Thank you for proving my prejudices…
>It doesn't, though. read this: https://serokell.io/blog/dimensions-and-haskell-introduction , then look into the referenced libraries. Have fun arguing with objective reality. As for resource safety, Haskell is yet to…
>Almost all formal verification in industry uses model checkers and sound static analysis. But does it happen because it is the only option or the best option? Also, encoding semantics specs is hard, so proper…
> if you ever find yourself interested in TLA+ Unlikely. Though I might be interested in HOL Isabelle eventually.
>I just don't see it for Haskell. https://gitlab.haskell.org/ghc/ghc/wikis/team-ghc Facebook and Microsoft do see value in Haskell.
>Sure, but let's say that it's a conservative estimate that 99% don't need proofs 99% don't need formal verification, they are OK with unit tests. If one is actually that concerned with an effort to perform actual…
>Also, I don't think that engineers are necessarily interested in proof, Depends on the area the engineer works in. Starting from some cost of failure you actually want a proper proof, because the inherent chance of…
I'm sorry, but how you can consider anything but deductive proof as a proof? Inductive 'proofs' are not strict proofs, they are suggestions that need to be tested. Well, except mathematical induction which is said to be…
> If you have a good specification mechanism that offers a choice of verification method, why do you need dependent types in addition? Because I don't see it as a good enough method. > There is no specific metric of…
>That they can be used in a useful way doesn't mean you should have them. It's a good enough reason to want them as an option. >Other things (like contract systems) can do pretty much what dependent types do If you want…
1. Problems with type inference is a problem introduced with polymorphism with implicit type variables and isn't exclusive to dependent types, 'f = show . read' shouldn't compile because of type ambiguity. What is so…
>More than anything it is precisely an exercise in whether dependent types are useful even if you aren't getting 100% watertight assurances with them. They are. Anyone working with linear algebra can tell that. Hell,…
> Basically: I need a Car Object with these exact fields vs give me a thing with the field "foobar" that contains something that I can concatenate with another things. Um, that's another matter entirely. Polymorphism.…
>If you argue that X is better than Y and Z because X is all you know, you just sound like a cultist. Learn first, argue later. Apparently, you didn't look in the mirror. Oh, well. Thank you for proving my prejudices…
>It doesn't, though. read this: https://serokell.io/blog/dimensions-and-haskell-introduction , then look into the referenced libraries. Have fun arguing with objective reality. As for resource safety, Haskell is yet to…
>Almost all formal verification in industry uses model checkers and sound static analysis. But does it happen because it is the only option or the best option? Also, encoding semantics specs is hard, so proper…
> if you ever find yourself interested in TLA+ Unlikely. Though I might be interested in HOL Isabelle eventually.
>I just don't see it for Haskell. https://gitlab.haskell.org/ghc/ghc/wikis/team-ghc Facebook and Microsoft do see value in Haskell.
>Sure, but let's say that it's a conservative estimate that 99% don't need proofs 99% don't need formal verification, they are OK with unit tests. If one is actually that concerned with an effort to perform actual…
>Also, I don't think that engineers are necessarily interested in proof, Depends on the area the engineer works in. Starting from some cost of failure you actually want a proper proof, because the inherent chance of…
I'm sorry, but how you can consider anything but deductive proof as a proof? Inductive 'proofs' are not strict proofs, they are suggestions that need to be tested. Well, except mathematical induction which is said to be…
> If you have a good specification mechanism that offers a choice of verification method, why do you need dependent types in addition? Because I don't see it as a good enough method. > There is no specific metric of…
>That they can be used in a useful way doesn't mean you should have them. It's a good enough reason to want them as an option. >Other things (like contract systems) can do pretty much what dependent types do If you want…
1. Problems with type inference is a problem introduced with polymorphism with implicit type variables and isn't exclusive to dependent types, 'f = show . read' shouldn't compile because of type ambiguity. What is so…
>More than anything it is precisely an exercise in whether dependent types are useful even if you aren't getting 100% watertight assurances with them. They are. Anyone working with linear algebra can tell that. Hell,…