1. 3

    Saved my hapless ass when I took category theory. Great resource.

    1. 1

      No matter what I do I still can’t get my head around category theory. Maybe I’ll try reading here more!

      1. 3

        As a large and constantly progressing area of advanced mathematics, I don’t think anyone can “get their head around” category theory ;)

    1. 2

      @hwayne ping! I am sure you have things to say.

      1. 7

        Fun fact, lobsters doesn’t actually notify you when you do that. But I saw the question and I should really write up my thoughts!

        1. 3

          Yes, please do! This thread needs your thoughts.

          1. 3

            This is going long and will probably have to be a newsletter

            1. 1

              I am looking forward to these thoughts and / or a newsletter!

              1. 1

                I look forward to it… but please address the very real world issue of DbC interacting (in both directions) with compilers, linters and optimizers and unit tests.

                I’ve been writing code in longish list of languages, from mainframe days to deeply embedded systems, in government scientific research institutes to commercial and industrial.

                I promise you, as I described above this is the route for formal methods to make a huge, and growing and very real impact on the world.

          1. 5

            I saw a lot of confusion on Twitter around what this is for. It’s very similar to systems like Souffle. There’s a great blog post about doing interesting static analysis using Souffle.

            According to the authors, Glean is a bit different in that it’s optimised for doing quick analysis, like for an editor or IDE. With Souffle, I have previously tried to analyse a medium sized Java code base using Doop, which consumed all memory and crashed.

            Hopefully Glean is more promising for this type of work. Sadly the Java indexer is not open source yet.

            1. 3

              Souffle

              Any opinions on how these relate to semgrep?

              1. 2

                For history: Semgrep was originally a Facebook project built upon their pfff project. Facebook stopped working on both of those so I guess Glean is being used as their replacement.

                From my understanding:

                • Semgrep has parsers and typers for all of the languages it supports, while Glean is designed to read data dumped out from a compiler
                • Pretty-printing and semantic diffing are part of Semgrep but wouldn’t really be feasible with Glean
                • Angle is a query language in Glean allowing abstraction of facts, e.g. you could define the concept of “type class” and have it applied to Scala and Haskell - it wouldn’t be based just on syntax patterns

                It’s say that Semgrep is more of a syntactical tool while Glean is a more full on static analysis tool.

            1. 1

              I never got my head around category theory in the way I’d like. Perhaps this will give me an example-based approach and help me to understand more. This is cool.

              1. 2

                This is a really cool concept, I miss these old utils.

                1. 1

                  I am really enjoying reading this article and look forward to continuing the series. I wonder if there are stories from the trenches, actually. I’d love to see some real world examples so I can learn from them.

                  1. 1

                    Really excited to see this based on the discussion I’ve been having with some folks on Twitter.

                    I’ve used Nom a bunch and am slowly becoming comfortable enough to prefer it to Pest for smallish projects. However, based on the above, I really don’t know how to think of it for language-related applications any more. I have lots of introspection to do and even more consideration to give this topic.

                    Either way, kudos to the nom team!

                    1. 2

                      nom is really good at parsing binary formats. It can have decent error messages too.

                      For programming languages, I would start with a PEG parser (one that can still produce decent error messages, such as lpeglabel - there is a nom-based PEG parsing library but I have never used it).

                      If the language becomes really popular I suppose I might move to a hand-written parser, but I’d maintain both to make sure the language has a proper grammar, and also because the grammar can often be easier to use in third party tools.

                      1. 1

                        make sure the language has a proper grammar,

                        What a good point!

                    1. 5

                      I am a huge fan of this software. It works great and I prefer it to my other favorite, tig, which seems a little less friendly than gitui does.

                      1. 2

                        thank you ❤️

                        1. 2

                          Yeah, thank YOU! I guess I need to spend some time learning how to configure things better and such. It’s on me to become a power user, expert operator, competent enthusiast, etc.

                          1. 2

                            Well there are probably a lot like you, so please consider making this a blog post, video or something - we will gladly share this on the project page :)

                        1. 3

                          I like serif monospace fonts, but this feels a bit too Computer Modern for me.

                          1. 3

                            Good call out, I think I agree with your assessment. Feels a bit more literary.

                          1. 9

                            I submitted a talk, let’s see if I get in!

                            1. 6

                              Now that I think about it, if I don’t get in, I may just release the video on my talks page regardless.

                              1. 5

                                I respect this attitude and think more people should do this. Or we could start RejectCon where you need to certify that your talk was rejected before you’re allowed consideration.

                            1. 1

                              I like this article, but I’m not sure why the title says “bare metal” when the tool is wrapping HDFS?

                              1. 12

                                It doesn’t need to use HDFS, and in fact that’s not the usual mode of operation. Normally it manages its own storage.

                                But in any case they’re using “bare metal” to mean that you can run it on actual computers, and not just as a component of some “cloud system” or other. Computing in the 21st century is weird.

                                1. 6

                                  It will plunk it’s files wherever you want. We’re running it on top of ZFS at my work, but it was previously on EXT4 (until we created too many files and discovered issues with truncated MD4 hash collision bugs with EXT4)

                                  1. 4

                                    until we created too many files and discovered issues with truncated MD4 hash collision bugs with EXT4

                                    This, alone, is fascinating. Is there a bug report or write up I could look over to learn more? It might make a good Lobsters submission on its own.

                                    1. 6

                                      I should preface this by saying we had create billions hundreds of millions of files before this was a problem. I believe this blog post goes over the symptoms and cause pretty well.

                                1. 2

                                  I have been watching Lean a little bit. Not sure where it stands on stability between versions 3 and 4. Does anyone have any insight into how the project is progressing?

                                  1. 4

                                    I can’t comment on Lean 3 versus Lean 4, but all of mathlib (the library where all the math development for Lean happens, including work in the cited article) is done in a fork of Lean 3. Porting everything to Lean 4 is work in progress; as far as I understand, Lean 4 is yet to be fully released (two pre-release milestones are public here).

                                    1. 2

                                      What a great reply. Thanks for the context and insight into mathlib. Really looking forward to digging in more.

                                      1. 4

                                        Happy to help :–)! Here are some more resources to save you some digging

                                        • Lean community is the main source of information on mathlib with lots of toolchain tutorials and API overviews such as this one
                                        • Project Xena, originally Professor Buzzard’s effort to formalize ICL undergrad maths curriculum, now also active as a more general blog and a Twitter account
                                        • Natural Number Game is a basic introduction, mentioned in both Xena and Lean community site, but worth mentioning here; it’s a very chill, slow-paced starting point that works entirely online!
                                        • Lean for the Curious Mathematician 2020 is a more advanced series of workshops with videos on YouTube, everything very recent
                                        • EPSRC TCC 2021 is another series of workshops, even more recent
                                        • And finally, the Zulip server is very active and people are very helpful!
                                  1. 3

                                    What I want to know is, where is the Rust equivalent of the Caddy web server (written in Go)? Axum isn’t it, right? If no such thing exists, why not? Did Caddy do it well enough that it killed the category, and it’s not worth writing something similar in Rust?

                                    I just want a simple binary that will host my websites for me and automatically sort out TLS certs, that “just works”.

                                    1. 7

                                      Caddy 2 well and truly killed the category for me. I even use it to reverse proxy the little things I’ve written in rust with rocket.

                                      I can literally think of almost nothing that I’d add to Caddy. Maybe WSGI/ASGI? But I haven’t missed that just running gunicorn or uvicorn behind Caddy.

                                      1. 2

                                        Do you have example configs for your rocket apps? Curious to see how it works up close. Thanks for an awesome comment.

                                        1. 4

                                          I wrote up how I host things in my basement behind a reverse proxy on a DO droplet, connected over wireguard.

                                          For rocket things, I skip the docker stuff and run rocket in my basement on an Ubuntu VM. The “Connect to VPN/Reverse Proxy” section on is the same. And the caddy configuration file is easy to write but (at least when I wrote all that down) was a little hard to google/ddg.

                                          stock-toolkit.tuxpup.com {
                                              reverse_proxy 10.20.30.3:8000
                                              log {
                                                  output file /var/log/caddy/stock-toolkit.tuxpup.com.caddy_access.log
                                              }
                                          }
                                          

                                          In that example, stock-toolkit.tuxpup.com was the public hostname for the app I was demonstrating. 10.20.30.3 was a FastAPI or Rocket server on a VM in my basement.

                                          That plus making my DNS point at that system running caddy is enough for caddy to set up a valid cert using LetsEncrypt, listen on 443, and proxy any connections coming in for that hostname to the backend. I have it logging each service to its own file because I use that to host several different things.

                                          1. 1

                                            This is really terrific! Thanks for the detail.

                                      2. 5

                                        I think all the necessary pieces exist as Cargo crates, but nobody has glued them together in a nice package yet. Paradoxically this may be the reason: it’s easy enough to DIY 80% of Caddy features yourself.

                                        1. 1

                                          Sounds like nginx with some additions, alternatively haproxy - dunno why I’d even want a rust version of that, you don’t RIIR something like that if you don’t have to. Think about how many issues nginx or apache2 will have to handle if they introduce rust and some people start being angry about unsupported platforms. And why would you do that if you don’t have to. There are nicer things to write in rust than to RIIR enterprise grade “middleware” and maintain that..

                                        1. 2

                                          While I’m sure there are more libraries that do this kind of thing, they’re kind of hard to find! The JSON Schema project lists a few of them: https://json-schema.org/implementations.html#from-data.

                                          1. 2

                                            Surely you’ve seen Quicktype on that list, right? It’s one of my go-to options!

                                            1. 1

                                              I didn’t actually find the json-schema list until after I wrote this library. But yes it looks very good!

                                              One consideration I’m not sure Quicktype handles (at a glance) is efficiently dealing with arbitrarily large inputs. For example, if I load 30MB of logs into DataStation, I still want to be able to show the inferred schema. I wasn’t able to do this (JavaScript would throw a stack exception) until I added sampling logic to this library.

                                          1. 5

                                            Quality is not negotiable. […] Our only measure of progress is delivering into our customers hands things they find valuable.

                                            I once asked Holub on Twitter what you should do if the client doesn’t consider security valuable. His response was something like “then don’t make it secure.”

                                            Edit found the thread, someone else was taking the hardline, but he was still handwaving away a lot of the concerns. I’ll be honest, I don’t really Holub’s online personality or any of his stances, so that might be coloring how I see this.

                                            1. 3

                                              “effective software development” occurs in a realm abstracted away from “software development that people with money pay for”.

                                              One would assume they were related somehow, but the computer industry has a long history of particularly successful businesses succeeding despite, rather than because, of their development practices. Alas, business success is then equated, by those desirous of business success, with Good/Effective Software Development practices.

                                              And so life gets worse.

                                              1. 3

                                                I think the comparison to radium/asbestos is apt, and ultimately while I try to practice some basic degree of professional ethics myself, I don’t think we can really dig ourselves out of this at scale without externally imposed regulations.

                                                See also: https://idlewords.com/talks/haunted_by_data.htm

                                                1. 1

                                                  I’ll be honest, I don’t really Holub’s online personality or any of his stances, so that might be coloring how I see this.

                                                  I appreciate your honesty and share your feelings. I find that Holub’s attitude tends toward the opposite extremes of “idealism” and, at the other end, “give them what they ask for” which can be hard to reconcile. I see shades of that extreme dichotomy of approach in this list.

                                                1. 6

                                                  I use Nushell quite a bit for data-driven workflows and find it a good replacement for jq and friends. Also a big fan of skim and been using Just instead of writing Makefiles recently.

                                                  1. 1

                                                    Just looks cool! it is similar to Earthly, but more for local dev rather than CI. Very cool.

                                                    1. 4

                                                      If you like Just, you’ll love Toast!

                                                      1. 2

                                                        We use Toast at work quite heavily. It’s been great!

                                                  1. 3

                                                    I am very curious to see more of Pijul both when it stabilizes and also when it becomes even easier to collaborate. Does anyone have any good comparisons specifically between Nest and GitHub/GitLab or equivalent? There’s so much potential here and I can’t wait to explore.

                                                    1. 1

                                                      Hi! I’m one of the authors of Pijul. Have you tried to install it? In any case, what’s specifically blocking you from contributing? We are definitely looking for contributors, a number of people are already doing great work, but it isn’t moving as fast as it could. I know the Nest is quite far, feature-wise, from older platforms like GitHub/GitLab, but we use it quite productively for Pijul itself (the CI hasn’t restarted after the fire, but will be restarted soon).

                                                      1. 1

                                                        Hi! I’m one of the authors of Pijul.

                                                        Hi there, I am so pleased you responded to my comment! First, please accept my heartfelt thanks for your efforts and congratulations on your progress. Way to go!

                                                        Next, kindly allow me to answer your queries in the detail I can.

                                                        Have you tried to install it?

                                                        I am on macOS predominantly for work and would love to be able to install it with Homebrew. I’m afraid that the last time I tried to install Pijul with cargo it didn’t work quite right, however this was rather far in the past. I shall try again with Rust 1.53 (which I believe to be the latest).

                                                        In any case, what’s specifically blocking you from contributing?

                                                        My company’s policies are rather restrictive when it comes to such things. I will see what I can do, however, perhaps to write some tutorials even as a start.

                                                        I know the Nest is quite far, feature-wise, from older platforms like GitHub/GitLab, but we use it quite productively for Pijul itself (the CI hasn’t restarted after the fire, but will be restarted soon).

                                                        These two things are really where the rubber meets the road, I’m afraid. The workflow like pull/merge requests and code review are really essential ingredients as soon as you get to n+1 engineers in my book. However, I’d be very interested in talking out some of the use cases! Ideally I’d love to be able to stand up my own Nest instance and get going that way. Obviously I don’t expect Pijul to evolve in quite the same directions as alternative projects like Fossil.

                                                        CI is also a really important part for me, as well. I wonder if it’d be sufficient for me to have pre-* hooks to ensure quality before pushing to a remote. This is something I can think about some more.

                                                        I hope that the above answers your questions and know that I am happy to engage in further dialog to the best of my abilities.

                                                        Love, +Jonathan

                                                        1. 1

                                                          Thanks for all the kind words! To answer some of your comments:

                                                          • There’s a basic review tool in the Nest, but (1) it has a bug where you can’t share your review with others, and (2) I feel it lacks a “todo list” showing you all the actions you need to take across all your projects.

                                                          • If you have a channel (named for example “main”), you can push to pseudo-channel “main/ci” to automatically merge if your changes pass the test.

                                                          We also have applications of the algorithms other than source code, so that could solve the chicken-and-egg problem where people want to use it “when everybody else does”.

                                                          1. 1

                                                            I appreciate your response. If there’s anything I can do to help out with testing the features I mentioned, let me know and I’ll gladly provide some feedback.

                                                            In the meantime, keep up the awesome!

                                                    1. 5

                                                      Bullet journalling has worked really well for me. Coupled with a personal wiki, it’s very powerful. Has anyone else had serious success?

                                                      1. 6

                                                        Yes, it’s great. I’ve been using it for 2,5 years in a manner similar to the article: Not artistic, just minimal and functional.

                                                        1. 2

                                                          Same here, been using Bullet journals for home and work for about three years, and really like it.

                                                          I previously had separate written books for work and home, but since Covid am now using a paper journal (small Leuchturm 1917 pocket book) for personal activities, and Emacs journal mode and org mode for work. Mostly because I don’t have the desk space at home to lay out my old work journal, but I’m enjoying being able to quickly take notes in meetings, work with tables, embed links, and keep track of citations from co-workers.

                                                          1. 2

                                                            Googling “journal mode” yielded a lot of org-journal links, is that what was meant? I’m curious

                                                            1. 2

                                                              Ah, correct, org-journal is the proper name. I had forgotten that it was part of org.

                                                              1. 1

                                                                I’m using org-journal for this purpose and it works really well for me. I do use it with a weekly file not separate daily files (for which it is designed it seems) and have each day as a top level org heading.

                                                            2. 1

                                                              What do you use for a personal wiki, and how do you take advantage of it with bullet journaling?

                                                              1. 2

                                                                I use Roam, mostly. Also, I keep todos and logs in the BuJo but information and such in the Wiki. Does that make any sense?

                                                                1. 1

                                                                  Yes. Thanks.