permeakra

6 ms·

1.
by permeakra 4y ago
> 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. Main
2.
by permeakra 7y ago
>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 right with this
3.
by permeakra 7y ago
>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 i
4.
by permeakra 7y ago
>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 verification of algorithmic
5.
by permeakra 7y ago
> if you ever find yourself interested in TLA+ Unlikely. Though I might be interested in HOL Isabelle eventually.
6.
by permeakra 7y ago
>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.
7.
by permeakra 7y ago
>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 ver
8.
by permeakra 7y ago
>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 error in incompl
9.
by permeakra 7y ago
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 a var
10.
by permeakra 7y ago
> 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 "strengt
11.
by permeakra 7y ago
>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 a sy
12.
by permeakra 7y ago
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 spe
13.
by permeakra 7y ago
>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, arrays tracking