1. 1

    Shoot, I really had my hopes up, here. Thought it was going to be about my favorite VAX editor.

    1. 6

      My favorite approach to this problem is in TLA+, and it always finds the solution.

      1. 4

        And here’s the Alloy way of doing it!

        1. 2

          Both of these are awesome! :) Thanks for the links!

      1. 3

        The single best advice I got from this talk is that I should watch this talk:

        Matt Might - Winning the War on Error Solving the Halting Problem and Curing Cancer

        Which was worth it, actually.

        1. 8

          I didn’t post this, but since it’s my talk I’d be happy to chat about it here.

          1. 3

            The “correct” pronunciation of SQLite (source: I attended a lecture by Dr. Richard Hipp) is S-Q-L-ite”

            1. 2

              “Type theory is a theory of computation that classifies programs according to their behavior, rather than their structure. Types are themselves programs whose values stand for specifications of program equivalence.”

              I had to stop right there. Most of us in imperative languages using types use them or structure. Especially in terms of structs or objects. This says types have nothing to do with structure. Makes me wonder if that’s inaccurate or type theory doesn’t cover what imperative/OOP programmers normally call types. Or do they have another definition of structure outside the mainstream definition. I have a feeling a certain amount of confusion that happens in type theory discussions might have started right there.

              Regarding the RedPRL prover, one person on it is the person who wrote Practical Foundations for Programming Languages. People might find those interesting by themselves.

              1. 8

                An example of something that structural interpretations of types have trouble with is equality of functions. Many programming languages have a very limited or outright broken notion of function equality, but it’s important if you want to prove a program conforms to a specification. It’s also important to have a language for what function equality means. Are a quicksort and a merge sort equal functions?

                Bob Harper is both the author of this blog post and PFPL.

                1. 3

                  Type theory is a theory of computation that classifies programs according to their behavior, rather than their structure. Types are themselves programs whose values stand for specifications of program equivalence.

                  I took “behaviour” to mean the ‘externally visible’ aspects of a value/program. For example, that something with function type Foo -> Bar can be called with a Foo value to produce a Bar value; that something with product type Foo * Bar can be projected to give both a Foo value and a Bar value; that something with sum type Foo + Bar can be projected to give either a Foo value or a Bar value but not both; etc.

                  I took “structure” to mean the ‘internal’ aspects of a value/program. For example, the different parts it may be made out of, any functions/computations that it uses (delayed or already completed), the syntax it was written as, etc.

                  In this sense:

                  • We can make these “behaviours” as complex and precise as we like, by making the types more complex and precise. For example, with dependent pairs and functions we can encode arbitrarily complicated mathematical relationships between values, inputs/outputs, etc.

                  • We can’t use types to classify the “structure” of a value/program.

                  As a provocative example, we can think about a value of product type Foo * Bar. We might think that the type tells us some ‘structural’ properties about the value, like “it contains a Foo” and “it contains a Bar”, but that’s not quite right. All we know is the “behaviour”, that we can project the value to get a Foo and a Bar, but we don’t know what will happen during that process. For all we know, the value might be an integer plumbed into an ‘unpairing’ function, like with Cantor pairing or Goedel numbering. Should we say that such a value “contains” a Foo and a Bar? What if that same integer is also used elsewhere to generate a boolean, a list of bitmaps, etc.? We’d at least have to weaken what we think of as “containing” or “structure”.

                  One example which I’ve heard discussed about type theory as opposed to set theory, is that in set theory we can (and very often do) ask whether a value is contained in a set, e.g. foo ∈ {foo, bar} and foo ∈ {high, low} are propositions which may be true or false. In type theory we can’t ask whether a value has a particular type, e.g. foo : (Foo * Bar) and foo : (High * Low) aren’t true/false propositions; they’re logical statements, which may be well-typed (valid) or ill-typed (invalid).

                  This is important for the “behaviour” vs “structure” distinction, since in set theory we can distinguish between isomorphic sets, e.g. {foo, bar} and {high, low} are isomorphic (they “behave the same”), but the foo ∈ x predicate is true for one and false for the other (they’re structured differently). Since type theory doesn’t let us do this, isomorphic types are indistinguishable (within the theory), so we can only reason about “behaviour”. This has connotations for modularity, reusability, optimisations, etc.

                  1. 3

                    You’re right that the types discussed in here are not being used in the same way that types in many c likes primarily use them. The goal is essentially different in scope. C types mostly capture the size of memory required for allocation of something. Types in the type theory sense can capture this idea, but can also contain much richer and complicated concepts in the types themselves.

                    also aside from PFPL Bob Harper is known for his work on SML and LF

                    1. 2

                      Yeah I don’t think you can do type theoretic proofs in say C# without a lot of work with interfaces and tuples. After all you don’t even have “Product and Sum types”. Heck it’s even hard right now in F# due to the fact that you have to explicitly name everything.

                      So for example say you have a function which takes a tuple of an int and (bool or string) and returns either a tuple of an int and a bool or and int an a string. int * (bool | string) -> (int * bool) | (int * string) //this would be the function signature. More amusingly

                      Old * (dumb | fat) -> (Old * dumb) | (Old | fat) // if I’m old and (dumb or fat) this implies I’m either old and dumb or old and fat

                      This is equivalent to A ^ (B v C) = (A ^ B) v (A ^ C). in logical propositions.

                      we can the write a function which takes an int and either a bool or a string, and return an int and bool, or an int and string and we know we have covered all possible return combinations.

                      In this way the function signature, the “Type” represents the lemma and then function itself exists as proof.

                      This as I understand it is merely the beginning of the whole thing. There’s a good computerphile video on the subject.

                    1. 12

                      It’s a good story, but the headline (just copied from CBC, not av’s fault!) is entirely wrong. Computer code didn’t put people in jail. An oppressive government put people in jail.

                      1. 1

                        I think both interpretations could be correct. The laws of the regime are wholly unethical, so I agree blame lies mostly with the government. But the Gülenists who created the link back to bylock did so knowing that innocent (in the eyes of the law) people might be incarcerated under the laws of the regime. The authors are partly culpable.

                        Of course, “Oppressive regime throws innocents in jail” isn’t going to get as many clicks.

                        1. 1

                          This is an excellent point. I’m not a Turk myself, but I hate Erdogan and the Islamist political views he represents. If Turkey were within my sphere of immediate political concern (rather than a country I have no particular connection to), I could easily see myself supporting the coup attempt itself, let alone a communications app connected with it. So seeing people legally exonerated for doing something that I think ought to be completely legitimate brings me no joy.

                          For an analogy closer to home, imagine that this article was about people trying desperately to prove that they were being falsely accused of using was Gab, because their jobs were at stake.

                            1. 1

                              I was thinking “Huh?” then saw you posted most of it a year or two ago. I’d say keep them coming but stay on practical papers or examples where possible. Shows relevance for readers who are curious about stuff or waiting until it’s practical to their needs. That’s been my strategy except occasional research result that was pretty interesting. Most of those get low reads/votes. So, I say stick with stuff where even the abstract tells you something practical and neat.

                            1. 2

                              This is awesome

                              One solution is to guard the value (second m) with a dynamic check. Another is to apply type tailoring to regexp-match!

                              If I understand this correctly, the type tailored code does exactly that, but is syntactically elided at each use of the macro. Right? Could this be extended to statically enforce constraints without run-time checks?

                              1. 3

                                I don’t think that’s right. As I understand it, the type errors are statically checked. The dynamic check is necessary in Typed Racket today due to designed-in limitations of the type checker, similar to how you must check for null in Java (although Racket does better than Java, IMHO, in that it conservatively rejects the unsafe code). The type tailored solution statically shows that the code rejected by Typed Racket is safe at compile time.

                                1. 3

                                  The type errors are checked statically, but only because the macro call expands to code that rebuilds the match function’s result. That checking has runtime overhead, including the list constructor and the if/error checks. What I’m asking is whether that cost can be eliminated.

                                  Surely some of it can: The occurrence typing could learn more about composites, so that you could traverse the list, asserting things along the way, without recreating the list.

                                  But some of it is less clear: Could you avoid the if/error checks completely with more knowledge of the relationship between the pattern and the return value? Could you do that only with a call-site macro, or do you need co-operation from the called code?

                                  1. 2

                                    I am admittedly hitting the bounds of my Racket knowledge here (I’ve written one or two macros in my life, so the bounds aren’t very big!), but as I understand the article and the macro it does statically use the value of the regex in the call, e.g.:

                                    smart-match rejects some programs that Typed Racket would accept, yet evaluate to runtime errors — for instance, (second (regexp-match "r" "racket")).

                                    So I think the answer is yes, you do have enough knowledge to do what you ask with a less trivial macro, but I’ll repeat that I’m out of my depth here!

                                    The return of their function is always a list, so I don’t see how you avoid that constructor as written. It would be neat if you could say, “Well, the only thing done with that list is to call second, so….” but that seems to be outside of the scope of the macro, if I understand correctly? I guess if all this concerned you then you could change the macro definition to say you wanted a specific group as an argument and then it might work?

                                    1. 3

                                      I don’t see how you avoid that constructor as written.

                                      There are two calls to the list constructor. One inside the match function that produces the result. And the other is in the macro expansion that takes that result and recreates it (exactly as is!) but throws a runtime-error if it violates some static assumption.

                                      I’m proposing replacing this:

                                        (car m)
                                        #,@(for/list ([i (in-range num-groups)])
                                             #`(or (list-ref m (+ 1 #,i))
                                                   (error 'smart-match))))

                                      with this:

                                      #,@(for ([i (in-range num-groups)])
                                           #`(or (list-ref m (+ 1 #,i))
                                                 (error 'smart-match))))

                                      Note the outer list constructor is gone, but more importantly the functional ‘for/list’ is replaced by an imperative ‘for’ that returns void.

                                      For an even simpler example of the sort of thing I’m interested in, consider this:

                                      (if (pair? x) (car x))

                                      vs this:

                                      (if (pair? x) (unsafe-car x))

                                      The first will check pair? twice. The second won’t.

                                      Presumably you could macro expand to unsafe calls, or the compiler could use constant propagation or global value numbering to eliminate the duplicate check. So my question (to the authors I guess): How can this “type tailoring” technique eliminate any check at all? Not just N -> 1, but 1 -> 0 checks.

                                      1. 3

                                        We want to convince Typed Racket’s type checker that the result of regexp-match has a second element.

                                        smart-match does this by unrolling the result into a list so that the number of results is syntactically apparent. For the given example, here is the actual program that runs after the smart-match macro expands:

                                        (let ([m
                                               (let ([m (regexp-match "(a*)b" "aaabbb")])
                                                 (if m
                                                     (list ; list constructor called with two arguments
                                                      (car m)
                                                      (or (list-ref m (+ 1 0))
                                                          (error 'smart-match)))
                                          (when m
                                            (string-length (second m))))

                                        Typed Racket knows that it is for sure safe to call second because it sees the list constructor called with two arguments.

                                        Your suggestion won’t quite work because for returns void, so the macro would try to splice void into the outer syntax object (#,@ is shorthand for unquote splicing), resulting in an error. (You can try it out, the post contains all the code needed to run the example).

                                        The actual implementation probably does use unsafe operators as you suggested though. (Actually, Typed Racket might automatically apply that optimization itself.)

                                        1. 1

                                          Thanks for posting this! I searched both your blog post and your paper for the expanded macro and I failed to find it. It would be a nice thing to put in the appendix of the post. Thanks for writing it; I enjoyed the paper!

                              1. 2

                                Intentional is Charles Simonyi’s company. They make very powerful DSL tools.If one wanted to say, “What will be the next Microsoft Excel in terms of bringing programming to the masses?” it would be a good place to look.

                                1. 3

                                  Note the first paragraph, which I’m paraphrasing here:

                                  “UPDATE: The story which follows was rushed to press before the facts were known and is wrong. The headline was clickbait speculation from the outset.”

                                  1. 2

                                    Dammit. Thanks for the clarification!

                                  1. 3

                                    COBOL will outlive us all. In ten-thousand years, when humanity has been replaced by gengineered simuloids, there will still be agents dedicated to maintaining their ancient COBOL subsystems.

                                    1. 6

                                      There was a joke in the Y2K era about a programmer who was terrified about the Y2K bug and had himself cryogenically frozen to wait out the tech apocalypse. 8000 years later he was revived into a techno-utopian future society. The first thing they said to him was, “We understand you know COBOL…”

                                      1. 1

                                        Good thing his cryopod wasn’t affected! Or maybe it was, and that’s why he required manual revival…

                                    1. 1

                                      Is using Orleans as a .NET Core cache a good idea? It has totally different architecture and durability goals than Redis (the default cache).

                                      1. 3

                                        Pretty good article which I mostly agree with aside from his assertions about most of curl’s bugs not being C-centric.

                                        1. 1

                                          …but a disproportionate share of the CVE bugs are, FWIW.

                                          1. 6

                                            My favorite two-short-article introduction to machine learning is A Few Useful Things to Know about Machine Learning [PDF] on the more positive side, and the paper you link on the more cautionary side.

                                            1. 5

                                              Probably the best title for any paper I have ever seen.

                                              In one brief phrase you understand what he is going to say, and with brief reflection, you know in your gut he is right.

                                              1. 2

                                                Oh that’s one I haven’t seen before.

                                                § 2.2 is a huge thing I’ve seen a lot of programmers get into the trap of simply because they forgot about what their model actually means.

                                                Thanks for that!

                                              1. 1

                                                There may be a line somewhere between “free for all” and “ban these sites”. What if there were a feature which would flag a site as “suspicious” and encourage submitters to verify stories elsewhere or look for a better source when submitting?

                                                1. 6

                                                  I don’t mind snark, personally. I actually thought the Reg article about the AWS outage was pretty funny.

                                                  1. 3

                                                    I don’t think it fits why people come here, though. 90% of the internet is insincerity, snark, and half-assed content.

                                                    1. 3

                                                      Yep, Reddit is full of snark and meanness, and a part of HN is people “well-actually"ing each other. I come to Lobsters for thoughtful articles and reasoned comments. Put another way, I would hope that no-one would comment on Lobsters with the same tone that The Register uses in most of its articles.

                                                      1. 1

                                                        I don’t think it fits why people come here, though.

                                                        I disagree. Otherwise those wouldn’t have been upvoted to front page

                                                      2. 1

                                                        I don’t mind the snark so much as the near-absence of fact checking. Stuff on The Register is often flat-out wrong, but if it makes for a good joke they’ll publish anyway.

                                                      1. 2

                                                        On first read, calling this “practical” may be overstating the case a bit, but interesting work nevertheless. They’re claiming a 100-fold improvement over other algorithms for computing the product of two encrypted integers, for example. Their security claims come from the partial approximate common divisor problem.

                                                        1. 3

                                                          This research has been mentioned on lobste.rs before, but this explanation may be easier to follow for many.