1. 22

The weekly thread to discuss what you have done recently and are working on this week.

Be descriptive, and don’t hesitate to ask for help!


  2. 14

    My rust bw tree embedded database is getting close to a place where I can focus entirely on performance and reliability! Theoretically it should be able to beat LSM trees on reads and traditional B+ trees on writes, occupying a nice tradeoff space. If anyone is into databases, lock-free algorithms, performance, making C API’s for rust stuff, or formal verification I’d love to work with more people on this, and I have a ton of time on my hands to collaborate for the next few months++ :)

    1. [Comment removed by author]

      1. 2

        jrnl has a feature to export journal files to JSON and Markdown. There wasn’t a feature to import a journal from a JSON/Markdown-formatted journal file, though, so I started coding that a few days ago. The JSON importer is pretty much finished but I haven’t done the Markdown one yet; you’re welcome to implement that if you happen to like Python. https://github.com/timetoplatypus/jrnl

      2. 12

        I’ve started learning Lean, working my way through the Introduction to Lean tutorial.

        Quoting their about page linked above,

        Lean is a new open source theorem prover being developed at Microsoft Research, and its standard library at Carnegie Mellon University. Lean aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs. The goal is to support both mathematical reasoning and reasoning about complex systems, and to verify claims in both domains.

        I also recommend watching Leonardo de Moura’s talks, From Z3 to Lean, Efficient Verification and The Lean Theorem Prover, for more about Lean.

        1. 6

          I’m interested in seeing a submission of your overall perspective of the Lean experience applied to practical examples after you’ve dug into it long enough. Especially compared to what you think the cost/benefits are versus methods that are lightweight (Alloy or TLA+), heavyweight (Coq or Isabelle), or programming-oriented (SPARK or Frama-C). Every experience report is potentially valuable.

          Maybe more so with you since your slides on Unit B were interesting. I’ll note that the interface/type-checking argument against TLA+ maybe not warranted. Maybe. TLA+ is often advocated as a supplement to coding something in a safe, programming language that lets you do things like that. As in, people who aren’t going to formally specify everything might use it as an extra tool on something that already checks interfaces. Turning it into a specification language with redundant features would be a drawback. You might be better off comparing to stuff aimed at fuller specifications such as Abstract State Machines, Event-B, VDM, or Z + SPIN/CSP as those were common in CompSci and industrial projects.

          1. 2

            I’m definitely thinking about writing up my experience with Lean once I’ve used it long enough.

            As for your comments on Unit-B, while I see where you’re coming from with your point about TLA+, I don’t think a nice type system is a redundant feature; especially if it’s advanced enough. Granted, I haven’t seriously TLA+ for anything yet; but one of the courses I’m taking at school this Fall uses it. So, I look forward to giving it a fair try and being able to better compare it with Unit-B.

            What I can say, though, is that TLA+‘s untyped logic seems to be quite nice in that it doesn’t tie your hands like a simple type system would. For instance, in TLA+ you could easily express heterogeneous sets (e.g. {5, {4}} is a set with an \Int and \set [\Int]) but whereas Event-B’s simple type system forbids you from doing that, Unit-B’s allows it via subtyping.

            Further, having a nice type system is quite beneficial:

            • Getting immediate feedback on your formulas before they’re even discharged to a solver or model checker. This speed would be invaluable if the method is to be integrated in everyday workflows.
            • Type-checking a specification can prevent you from spending time implementing an inconsistent spec. It is even more important considering that type-checking the implementation won’t reveal the same information. So, being able to quickly get feedback on your spec before going off spending time implementing it is really useful.

            Lastly, I’ve thought about writing up a detailed comparison of Unit-B with a few other methods of different shapes and sizes (Event-B, TLA+, Lean) by working through one or more examples in each. Hopefully I’ll be able to do that after Fall.

        2. 7
          1. 7

            Started a new collaborative project to document the history of expressive systems. Will be both an online resource and workshop series. Still working on the first version of the online resource, but our proposal for the first workshop was accepted and will happen in November in Portugal.

            I had both vacation days and hotels.com points expiring at the end of August, which was impetus to take a one-week vacation last week to Bude, in north Cornwall. It was nice. I walked a bunch on the South West Coast Path, and along the beach north of Bude. At low tide you can walk about ~3-4 miles along the beach below the cliffs, though sections become impassable at high tide. I avoided doing any “regular” laptop-related work, but I did take a research notebook with me to jot down any ideas that came up, and found that way of working quite productive; filled up about 25 pages and have at least two papers sketched out now. (Maybe I should take more vacations to boost my productivity.)

            Now periodically reloading Houston stream gauges to see how my parents are doing (they’re ok so far).

            1. 6

              Work: Looks like I am getting ahead of the reporting and can get back to work on crazy changes in the FreeBSD network stack.

              !Work: Writing drivers to handle the power stuff on this crazy little laptop I have. Amazing how drivers spring up when datasheets are available.

              1. 2

                What laptop is that? Looks neat!

                1. 2

                  Looks like a GPD Pocket. What keyboard is that?

                  1. 2

                    It is an MIT-layout Planck. Parts are regularly available and MassDrop occasionally runs group buys for kits. I am waiting for the current group buy to ship, though it has been delayed ~10 weeks because they neglected to plan for FCC Part 15 certification.

                  2. 2

                    It looks like it could be just the thing for an on-call support engineer - you could toss it into a small bag and take it out to the pub, restaurant or whatever. You can do that with a MacBook, but they’re really that light or small, and you really don’t want to forget your bag with one of those in it.

                2. 6

                  I recently built a little “save to eval-able code” serializer for PISC, so that I have a way to save/load state for a video game I have planned.

                  I’ve also been working through some PicoLisp tutorials, as a small start on what I expect to be a year or two spent investigating LISP/Scheme and seeing what I can learn from actually doing something in LISP, rather than just reading about it or bouncing off of it. (I might also go through the SICP at some point).

                  Once I get through the tutorials, I have some plans around writing some basic code generation for covering the corners of C# that are a bit awkward to write by hand right now, such as immutable classes. You have to repeat yourself a lot in those, when you really just want to give the class name, and a list of type/name pairs.

                  I’ve written something similar for pisc here, but using PicoLisps app framework to build a GUI, and then maybe exploring how to customize said GUI seemed like a decent nights/weekends project for getting my feet wet and deciding how much more time I’d want to put into it.

                  1. 5

                    I’m working on a Markdown to PDF service, via latex.

                    Still wondering if creating nicely typesetted PDF from Markdown is of interest to anyone though!

                    1. [Comment removed by author]

                      1. 2

                        Thanks for the feedback, your experience is very interesting!

                        Is there a better layer of abstraction if I want to avoid generating PDF directly? What’s appealing to me in tex is that it already takes care of most of the typographic choices.

                      2. 1

                        Remarq does this. I regularly recommend it to consultants and small businesses for producing nice-looking reports quickly and cheaply.

                      3. 5

                        I’ve been working on a data querying tool - need to fix some bugs, schedule some user review sessions, and revamp the homepage based on what I learn.

                        1. 4

                          At work, I’m finishing up a migration to a new CMS.

                          At home, I’m going to put together another track soon. My SoundCloud if you’re interested: https://soundcloud.com/nick-jurista

                          1. 4

                            Writing a whole lotta test cases at work and reworking a lot of my material for a computer networking course I’m teaching. so if any of you know about great youtube videos about networking theory / nice graphics / other things I might be able to use, I’d appreciate a link and I’ll buy you a beverage of choice if we ever meet ;)

                            1. 3

                              I’m studying deep reinforcement learning and playing around with rl4j. I’m also considering to start a text plotting library for python because there are only a few clusmy wrappers for gnuplotlib and none of them works decently. I need this for another project that it’s currently stuck because of this.

                              1. 2

                                Work: writing mawr scrapers, finishing up a prototype of a new logging system for our crawler nodes, ever so slowly increasing test coverage.

                                Outside work: just got my website on HTTPS finally, trying to refine some writing on sockets and their implementation in Python, updating my resume, etc.

                                1. 2

                                  I’m starting with the refactoring of a huge chunk of the code in one of the main projects at my company. It’s my 3rd week at the job ;)

                                  1. 2

                                    At work I’ll be setting up Magento 2 in a virtualized environment all the while I continue to debug issues with our staging environment and working on changes for a mobile redesign.

                                    In my spare time I’m making some theme and bumper music for a friend’s podcast.

                                    1. 2

                                      I’m working on https://www.helmspoint.com . It helps you deploy machine learning keras models. All you have to do is upload your weights and declare your architecture, and hit publish, and you’re done.