curryhoward

10 ms·

31.
by curryhoward 6y ago
My number one use case for comments is documenting invariants/preconditions/postconditions that are not enforced by any automated mechanism (e.g., a type system). I'm surprised no one else has mentioned this. To me these are
32.
by curryhoward 6y ago
There is a recent paper called "Codata in action" [1] that I think gives a nice explanation of (part of) OOP in terms of codata types. But that paper also finally clarified for me why OOP is so awkward and unnatural sometimes. Why
33.
by curryhoward 6y ago
> Union types are basically an anonymous form of sum types. This is false on multiple levels. First, being a sum type has nothing to do with the type being named vs. anonymous. What makes a sum type a sum type is that it's a categor
34.
by curryhoward 6y ago
When you say "Rust enums are also enums", that's not true in general. What is true is that _some_ Rust "enums" (like your `Colour` example) can be represented as traditional enums. You don't prove a universal q
35.
by curryhoward 6y ago
That's right. It's unfortunate that Rust calls them "enums", since as you noted that term already had a well-established meaning in other languages, and the concept that Rust calls "enums" also had several exis
36.
by curryhoward 6y ago
Did you mean to reply to a different comment? You seem to be restating the correct part of orthoxerox's comment. I was merely refuting the incorrect part.
37.
by curryhoward 6y ago
I love seeing new Haskell projects, though I personally would rather just stick with Haskell's clean syntax: data Maybe a = Nothing | Just a ...over this: data Maybe<a> { Nothing, Just(value: a) } I unders
38.
by curryhoward 6y ago
That's true in practice, but technically speaking it's false. You could imagine a contrived system which is not Turing complete but still contains a (rather useless) primitive that causes an infinite loop.
39.
by curryhoward 6y ago
I'm guessing the comment was talking about examples like this: program -abcdefg.txt Just from reading this, you can't tell where the flags end and the filename begins unless you have all the flags and their arities memori
40.
by curryhoward 6y ago
> I am talking about (1) the proof steps involved in proving a given, fixed statement. You are talking about (2) a wider notion that includes the formulation of the statement to be proved. No, I am not. The original proof used an implici
41.
by curryhoward 6y ago
> The article doesn't say that the original proof was incorrect. The article very clearly points out an error in the original proof. The HN community can be so toxic sometimes. Inevitably whenever someone produces a new machine-chec
42.
by curryhoward 6y ago
I feel like most commenters are missing the point. The fact that this issue was finally settled once and for all using a proof assistant is a huge achievement! That's the highest degree of scrutiny that a proof can undergo. This is esp
43.
by curryhoward 6y ago
In academia, "type theory" almost always means dependent type theory, such as Martin-Löf type theory or homotopy type theory. Type theory is used in most theorem provers as a foundation for mathematics. The title of this blog post
44.
by curryhoward 6y ago
Content editors should not be able to add arbitrary code to a bank's website unless it undergoes review from someone who understands web security. If there is some kind of content editing tool, it should only allow content (not arbitra
45.
by curryhoward 6y ago
Another implementation of this idea: https://www.huffgram.com/
46.
by curryhoward 6y ago
> For ‘moderate performance’ surely JVM based languages are what you’re looking for? There’s great tooling and a very low barrier to creating new languages. Not sure I understand what you're suggesting. I was asking for a language w
47.
by curryhoward 6y ago
> It’s already suspicious by virtue of having a hand-wavy "Int" type (what size/signedness is that?) and it appears to be object-oriented (so we have to rely on compiler optimisations to remove dynamic dispatch) and garbag
48.
by curryhoward 6y ago
I completely sympathize with the difficulty in understanding the notation and wish it were more accessible. I struggled with it for some time. But as someone who eventually learned it, I find it to be fairly sensible. What would be a better
49.
by curryhoward 6y ago
`A` is a type, yes. Whether `Type` is a type depends on what type system you're working in. If `Type` is its own type, then it turns out you can use that to do infinite recursion (this is called Girard's paradox). Dependent types
50.
by curryhoward 6y ago
> AFAICT Coq doesn't have linear types, and thus can't provide in-place modification of array elements or non-reference-counted/GCed non-primitive values, which means it can't take full advantage of a real CPU+RAM mac
51.
by curryhoward 6y ago
Unfortunately you need to know type theory/logic notation in order to read this. Here's the English translation: - There is a variable called `x` in scope. - `x` is known to have type `A`. - `B` is a function that, when given `x`
52.
by curryhoward 6y ago
> The problem is that, as far as I can tell, there is no language with zero-cost dependent types, i.e. a language with dependent types that has a subset equivalent to Rust that compiles to machine code as efficient as the Rust compiler o
53.
by curryhoward 6y ago
Maybe with shelter-in-place I'll have time to write it. :) > I'm curious, are there languages that in your opinion support dependent typing well enough to allow all the concepts that you are describing? Most of my experience wi
54.
by curryhoward 6y ago
I've been meaning to write a tutorial on dependent types, but aimed at programmers rather than mathematicians and computer scientists. Here are some of the reasons I love them so much: - The most popular motivation: the ability to writ
55.
by curryhoward 6y ago
I agree with the other commenter about the comma in this sentence. But I'd also like to point out that 100% error-free code is possible. There's a whole branch of computer science dedicated to it: formal verification. I personally
56.
by curryhoward 6y ago
This looks a lot like Toast: https://github.com/stepchowfun/toast
57.
by curryhoward 7y ago
The question you were answering was not talking about proof search. It was merely asking whether it was possible to do verification in the same language that the program is written in. And, contrary to your response, it is possible to do ve
58.
by curryhoward 7y ago
Not if the human provides the proofs and the compiler merely checks them (like in Coq, for example).
59.
by curryhoward 7y ago
Consider these equations for integers: x * 1 = x 1 * x = 1 x * (y * z) = (x * y) * z These should be familiar if you know about integers. Now consider the following equations for strings: concat(x, "") = x
60.
Write Out Unicode in Octal(lubutu.com)
1 points by curryhoward 7y ago|0 comments

More ›