1. 1

    Interesting result. Even more interesting that it’s come out of AOL. I figured AOL was dead – not the case. They’ve pivoted into adtech. Nice that they’re publishing some of their work!

    1. 3

      I’ve been a big fan of e-paper for years. I owned two of the old iRex iLiads a decade ago when they were first released in the US, and currently have a Kobo Mini.

      I’ve been eyeing a larger-factor reader for PDFs – the Mini is great for reading fiction in various formats, but A4 and Letter PDFs just don’t scale well to that size. This might fit that bill (eventually, provided it ships).

      At the same time, I write daily paper todo lists, and regularly take paper notes. It’s not something I ever really considered using e-paper for (well, not for years, anyway – the iLiad had a hand-annotation capability, but it was clunky, slow, and generally unusable). I’m not certain it makes financial sense yet, but I’d be willing to entertain going digital with my notes if this comes close to fulfilling its promises. Still, that’s a further goal than “just shipping”, which is still uncertain.

      All that said, at this point my major requests would include: 1- opening the spec up (too many devices get abandoned, and being able to install custom firmware makes the investment much more enticing), and 2- allowing (even limited) use of non-first-party styli (having to spend $80 or more for a spare becomes a pretty hard turnoff pretty quickly).

      1. 2

        I bought the first kobo when it came out, and its still working (Mostly) great. Ebooks are great for fiction, but mostly fall apart when dealing with technical books, as I find it much easier to flip around an actual paper book, the physical memory of where stuff is is worth a lot.

        1. 4

          I tend to agree, though I have thoughts on the matter.

          Books work well, but I’ve also found that reasonably-designed websites work almost as well. A good index and quick access to tables of contents go a long way. Plus the ability to bookmark things and use the url bar to go back to frequently-used pages.

          Which means, I think, that a decent tech-reference ereader is achievable. It’s just that the interfaces have so far all been designed for linear reading rather than browsing and flipping. Which makes sense for high-latency page refreshes. Now that e-paper is getting faster, though, we might be getting close to something more useful for tech reference.

          1. 1

            How fast is epaper getting? The FAQ for the reMarkable says 50-60ms, which is still awfully slow for me. Probably great for reading, but terrible for note taking. I’m very sensitive to computer notetaking interfaces. I still use lots of dead trees and my favorite pen. I’ve tried 4-5 different tables and dozens of apps and 6-7 different styluses, and absolutely nothing is “good enough” for me to ditch my pen and paper. When I want an archive, I just take scan my pages on a flatbed.

            The FAQ mentions “four years” of getting the UX to actually feel like paper. They explicitly call out friction between the stylus and the display, which has always been one of my big “eh, still not as nice as a pen or pencil” for every tablet/stylus combination I’ve tried. It’ll be interesting to see how reality lives up to their claims if they deliver, but I’m not hopeful.

            I’ve also been wanting an ereader for PDFs, especially research papers and maths-related things. This could fit the bill, but it’d be a hard sell for me.

      1. 3

        Let me preface this with saying thank you and I am not ungrateful I just want to spur some conversation.

        How complicated is U2F to implement, would it work for Lobsters, and is there a reason it wasn’t done this time around?

        If it hasn’t been done because it wasn’t thought of or there wasn’t time, then it’s a great opportunity for someone to send a PR :)

        1. 2

          There’s a couple of different U2F gems, and none of them look hard to use, but to test it you’d need a U2F token or token simulator. If there’s a good way to test U2F support without messing around with Yubikeys, I’d love pointers.

          1. 3

            I don’t know about “good”, but Google has implemented a software U2F token in Java. Firefox also has the security.webauth.u2f_enable_softtoken pref, which will let you test use of U2F on the web without a hardware device. You can see the implementation here.

            1. 1

              Thanks! This is relevant to my current interests. :)

        1. 5

          The linked thread was one of the few times I made a counterpoint on HN followed by the author showed up saying the counterpoint was effectively the roadmap. It was good as I was just passing on what Dresden & NICTA had already done. Less surprising he was working at NICTA on seL4. ;) In any case, I later discovered Redox was using some similar techniques with them in much more production form but with less security at foundations. There might be opportunities for the projects to work together if they’re not already. The components for one might be reusable in the other if the OS/microkernel-level stuff is hidden in modules well.

          I also agree with Nagle that this has potential for use in things like routers. The reason being message routers, guards, and VPN’s were first things the security kernels were used for. They did well during evaluation. Separation kernels and security-focused microkernels followed them with seL4 being highest in development assurance. It also has a Linux layer & ARM support. Gives this project extra potential in medium-high assurance security if they just do their components well. Code from Netbricks could be ported to it for first appliance.

          EDIT: Author of project posted same story at link below. You might want to glance at it Wednesday in case the author adds any interesting details by then.

          https://news.ycombinator.com/item?id=13267724

          1. 5

            Thanks for pointing me to this! I have a lobste.rs account but I don’t tend to use it very often. Indeed our first “usecase” is network appliances. But it’s a ways down the road. I’d personally love to see a seL4 implementation of Xen’s hypercall interface, and slowly start replacing a Linux etc dom0 with high-quality isolated seL4 components. My primary motivation for working on this project is that I think it’s fun, I’ve been learning a lot, and I have the time while I’m still in school.

            1. 2

              Well, by all means keep doing the work for fun and enlightenment. Always justified. :)

              Not sure if Xen’s stuff will be securable since it wasn’t designed for it from start. If API is, then that implementation could benefit in that all kinds of stuff targeted to Xen would be immediately usable. That includes MirageOS.

          1. 1

            Well, about time I change my habits.

            Don’t have 2FA enabled for manager. .

            1. 1

              2FA secret keys were allegedly compromised as well, so in this case that wouldn’t have helped.

            1. 5

              This is my project if you have any questions! We have a mailing list and IRC channel if you’d like to get involved, or just say hi.

              1. 4

                The green padlock doesn’t always mean “trustworthy”; just “encrypted.”

                Nitpicker’s corner: Browsers should only show green if it’s an EV cert, which Let’s Encrypt does not offer. Browsers will do blue or something otherwise.

                1. 3

                  That’s not the case in Firefox, at least - with EV in Firefox it just additionally shows the organization text next to it

                1. 12

                  Tried to signup to start playing, got:

                  Username is too short (minimum is 5 characters)
                  

                  Why do people do this?

                  1. 4

                    I imagine it’s to stop people from fighting over 2 and 3 letter names.

                    1. 4

                      I’m always sad to lose my 3-letter name. I feel a good deal of ownership over it being that it’s my actual middle name!

                      1. 4

                        Yeah, I’ve been jfb pretty much everywhere since 1992.

                        1. 3

                          it’s one thing to lose my preferred nick to another Douglas Adams fan, but i was rather peeved when some couple named zander and emily decided they wanted a joint twitter account named ‘zem’ (: (they seem to have since given up on it; the current zem@twitter is someone whose actual name is zem, which arguably gives her a greater moral right to it)

                          1. 3

                            “zem” for Zander and Emily seems entirely legitimate to me.

                      2. 3

                        I also had this sad moment :( Enough services do this that I’ve a canonical 6-letter extension: cmrx64.

                        1. 2

                          I hate to break it to you, but there are sites insisting that your username should be more than 8 characters long ^^

                          1. 1

                            He just upgrades: cmrx1024

                            1. 2

                              more than 8

                              1024 brings him exactly at 8 which some sites still refuse :D (hint: count the chars in my nick). He would have to upgrade to cmrx16384 which isn’t that catchy anymore ;)

                      1. 1

                        The first thing that struck me from Lamport’s examples here of structured proofs is how similar they are to a common way K-12 math initially teaches students to write proofs, the “two-column proof” structure. A two-column proof has a sequence of numbered statements in the left column, each of which must be justified by reasons noted in the right column. The reasons can be either appeals to a previous numbered statement, or to a named theorem/lemma already introduced in the textbook. Instead of using the second column, Lamport instead writes “PROOF: …” and gives the justification below each numbered statement, but it otherwise seems pretty similar.

                        The other main difference, of course, is that he thinks it would be a good idea to use this in professional mathematics work rather than only in pedagogy. This brief dismissal is probably representative of the opposite view. It’s a bit surprising that Lamport therefore didn’t discuss two-column proofs (perhaps he hasn’t run across them?). He makes it sound like mathematicians haven’t thought of writing proofs this way, when I think the current situation is rather than they’ve thought of it and even teach it, but consider it only useful as a pedagogical tool, and too cumbersome for real work. That’s the part he really needs to convince them is wrong.

                        1. 1

                          Every time structured hand-written proofs come up, I think of my 9th grade geometry class where we learned how to do two-column proofs. At least for me, the presentation was far too informal for it to really “click” with me what the core rules of logic were. Recently I’ve been learning how to use Isabelle/Isar, which is a structured proof language built on top of the Isabelle proof assistant framework. It’s quite refreshing compared to the usual unstructured proofs in Isabelle or Coq. In my personal education, learning how to reason with natural deduction-style systems was hugely helpful for actually learning at a deep level how proofs and logic mix together and work. I think there are some serious improvements that could be done to early math education using more formal systems.

                          I’m not a professional mathematician (yet) and can’t comment on any issues there. I will point out the growing Archive of Formal Proofs, http://afp.sourceforge.net/. It seems promising!