ebingdom

14 ms·

31.
by ebingdom 4y ago
Yeah seriously. I'm surprised by the other comments here. It seems like people want loosy goosey typing that magically inserts lossy casts with convoluted semantics, as if they've been brainwashed by JavaScript and C.
32.
by ebingdom 4y ago
I personally love that Rust doesn't automatically convert between different types of numbers, with different precision and rounding/overflow behaviors. If I'm multiplying numbers of different types, I want the compiler to for
33.
by ebingdom 4y ago
> The reason for that is that it is not nice enough a logic, full stop. So why would it be nice enough for computer scientists? Type theory has many attractive properties over traditional foundations like set theory. See, for example: h
34.
by ebingdom 4y ago
> First, theorem proving is NOT the same as an advanced form of static typing. This Hacker News post is about a theorem prover based on dependent types. That's the context for our discussion. > You will still have buggy programs
35.
by ebingdom 4y ago
> Let's take a CAD program. Which aspects of it would you formally verify? Any large program will contain some smaller components with relatively well-defined behavior. CAD is not my specialty, so I can't really comment on what
36.
by ebingdom 4y ago
> Try to prove correctness of a CAD program, for example. Or of a graphics card implementation. Or ... You don't need to verify the entire program for formal verification to be useful. You can adopt it incrementally. The most common
37.
by ebingdom 4y ago
> The threshold is mathematicians opting to use these tools themselves for their work. There are not many mathematicians using them so far. The kinds of theorems that we need to prove in software are much more elementary than what mathem
38.
by ebingdom 4y ago
No, docandrew is correct. You are incorrectly applying Rice's theorem. Rice's theorem states that those properties can't be automatically decided in general. But that's irrelevant to this discussion, because this "m
39.
by ebingdom 4y ago
Checking proofs is decidable. Coming up with proofs is undecidable. This tool does the former, leaving the latter up to humans.
40.
by ebingdom 4y ago
That's not what Rice's theorem states. Rice's theorem states that interesting properties are undecidable, not that they can't be proven. Undecidability is not relevant when you are providing the proofs to the computer.
41.
by ebingdom 4y ago
> Isn't Lean HoTT? No. Lean is good old fashioned Martin-Löf type theory. HoTT is that type theory + univalence + higher inductive types. Lean actually has proof irrelevance, which is incompatible with HoTT. But the good news is you
42.
by ebingdom 4y ago
I was with you until: > 5) Too much gratuitous abstraction. The old version was "everything is predicate calculus". The new version is "everything is a type" and "everything is functional". Total functional
43.
by ebingdom 4y ago
> However, every time somebody starts going negative on formal verification by talking about decidability, I get itchy. Sure, we know, all interesting properties of programs in all interesting languages are undecidable in general. Rice&#
44.
by ebingdom 4y ago
> It's the same with a programming language: if it's designed too spartan, I have to write too much code that is always similar, which causes effort and obscures the real intention of the code. I think Go is the perfect example
45.
by ebingdom 4y ago
Just because something is popular doesn't mean it's right.
46.
by ebingdom 4y ago
Rust's "enums" also include products. Each case can have multiple arguments. That's a sum of products. "Algebraic data type" is the proper term for what Rust calls "enums", since they encompass both s
47.
by ebingdom 4y ago
I'm pleasantly surprised by these comments. A few years ago people were so entrenched in their object-oriented upbringing that sum types were considered "weird functional stuff" and thus unsuitable for "real" work (
48.
by ebingdom 4y ago
I'd say it just as you did but with "algebraic data types" instead of "enums".
49.
by ebingdom 4y ago
Although an improvement over C, Go seems to have the same unofficial motto: "I don't need you to X, just trust me to Y", as in: 1) I don't need you to prevent me from mutating this variable, just trust me to not mutate i
50.
by ebingdom 4y ago
I just can't get past the fact that Go doesn't have sum types. As someone who dabbles in category theory, it makes no sense to me that so many popular languages have product types but not their categorical dual. The lack of sum ty
51.
by ebingdom 4y ago
What if Bob never gets the confirmation from Alice in step 5? Or if Bob doesn't need it, why did Alice even send it?
52.
by ebingdom 4y ago
> You spend time on reddit because you want to. It seems unproductive to tell yourself that you don't. This seems like a mischaracterization of how addiction works.
53.
by ebingdom 4y ago
Did you reply to the wrong comment?
54.
by ebingdom 4y ago
Looks interesting, but does it offer any unique features that set it apart from other such languages like JSON, XML, etc.? I see that matrix example, but is it any different from an array? (I couldn't tell from reading the docs.)
55.
by ebingdom 4y ago
> it's much more basic than ebingdom's explanation Just to contextualize my explanation, I took it as a given that we were talking about the two _safe_ ways to handle missing data: a type system which has a notion of nullable&#
56.
by ebingdom 4y ago
No, the type for `get` would only have a single layer of `Option`. But V is a type parameter, so you can instantiate it with another layer of Option. You don't need to (and shouldn't) modify the type signature of the `get` method.
57.
by ebingdom 4y ago
Rust's traits are a limited version of Haskell's type classes. They are more limited in at least two ways: 1. Rust's traits are unary relations (i.e., predicates) on types, whereas Haskell's type classes support relation
58.
by ebingdom 4y ago
Personally, I've had the opposite experience. Rust is one of the few languages that has proper support for algebraic data types and pattern matching, which I consider table stakes for a programming language. I know that's not what
59.
by ebingdom 4y ago
This is terrible reasoning. You're basically saying that language features have no impact on bugs, putting all the blame on the programmers. But programmers are humans, and as such they make mistakes (even the best of us). We should em
60.
by ebingdom 4y ago
> It’s worse in every way to null. No, Optional is actually better than null because it's functorial. That means it obeys some common sense laws that one might intuitively expect. Instead of reciting the functor laws, I'll give

More ›