lower

> It'd be really nice to see the code released!

I'm surprised the conference accepted the paper without the source code being made public.

> a few thousands lines of code when I looked at it a while back.

That's not true anymore. Have a look at CompCert, CakeML or CertiKOS, for example. Verification still takes a big effort, but it's getting better a lot.

> Here Mozilla is trying to verify it’s crypto.

If you look at the paper describing this work <https://arxiv.org/abs/1703.00053>, you'll see that this is an academic effort and 7 of 12 authors are actually at Microsoft Research. But kudos to Mozilla for bringing all this advanced stuff to their products.

Is evince actually still affected? The article says that it was affected initially (i.e. six years ago), but that the bug has since been fixed.

Both Okular and Evince use poppler for pdf rendering, so they should both get the fix from poppler.

There is a setting to enable suggestions also in the location bar (off by default, I think).

In what way is ANTLR better than bison?

I (German) have never used NFC payments and was curious how that would work with my bank. Turns out they want me to install an app on my phone for this, which is definitely not going to happen.

You know what happens to many bike lanes in winter around here (Germany)? The snow from the road gets heaped on them... It's usual for people to ride on the road then.

It depends on how much snow you get. Normal tires are fine on snow once you get used to it. So if you have icy conditions just for a few weeks, it's probably not worth the hassle to switch. (I've been riding a road bike throughout all winter for more than a decade now. Riding on snow is fine. The only dangerous situation in winter is actually on warmer days without snow, where one doesn't expect anything, but when the road has frozen over invisibly in some dark corner.)

I've been using this for a while and am very happy. Especially the ability to use a private git repository for synchronization of laptop and desktop makes this convenient.

> Or, worse, adopt it as the way to do things.

Thompson, Ritchie and Kernighan admit that Unix was a prank

http://www.stokely.com/lighter.side/unix.prank.html

I remember this from a similar example in C:

   #include <stdio.h>
   int main()
   {
       int x = 10;
       while (x --> 0) /* x goes to 0 */
       {
          printf("%d ", x);
       }
   }

(prints 9 8 7 6 5 4 3 2 1 0)

https://stackoverflow.com/questions/1642028/what-is-the-oper...

Yeah, do it! :)

Your definition of order is not the standard one!

Usually one would have:

    zerothOrderFunction :: a
    firstOrderFunction :: a -> b
    firstOrderFunction' :: a -> (b -> c)
    SecondOrderFunction :: (a -> b) -> c

After all, the functions firstOrderFunction and firstOrderFunction' are the same up to currying.

The standard definition of order is given here (at the end of the section):

https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus#T...

It's nice to have a small example of how to compile to LLVM, but the compiler is a bit more limited than what the blog post makes it appear.

It's not quite `a compiler for simply typed lambda calculus', but only for a small fragment without higher-order functions. One currently cannot write lambda terms that take functions as arguments.

I was curious how the compiler represents closures and manages memory, mainly because I'm looking for a small example of how to do garbage collection in LLVM. But it turns out that the parser doesn't allow function types yet and the compiler itself doesn't implement closures yet.

The OCaml implementation used to be hard-coded in the type system, but has now been rewritten (in 4.02, I think) using GADTs.

https://ocaml.org/meetings/ocaml/2013/proposals/formats-as-g...

https://caml.inria.fr/mantis/view.php?id=6017

The compiler only does syntactic desugaring of format strings now.