Threads for meithecatte

  1. 1

    Still to this day, my favorite pattern for UUIDs is to serialize a small amount of relevant metadata (enrollment year, name, student id, in this case) and encrypt / pad that byte string.

    It looks like any-ole uuid at first glance, you can pass it around safely, and you can retrieve that data quickly without DB round trips or regex. Great for request validation too!

    It still suffers from the ‘embedded logic’ argument, but I feel like changing uuids is a no-no anyway.

    1. 3

      A name is something that can change. The ID is probably something you want to stay the same.

      1. 3

        If any of that changes for any reason, your ID has to change if you rely on it anywhere.

        I can see fat-fingered entry of all of those fields causing you heartache.

        1. 1

          Be careful about trusting data like year read from this, because encrypted data can still be manipulated. In UUID you most likely won’t have enough bits left to add a proper HMAC.

        1. 10

          Ah, yes, printf(3), the well-known OCaml function.

          1. 3

            The quality of this explanation is stunning. It is the first time I’ve seen FFT explained such that the complex roots of unity are an obvious solution, and not some convoluted math with no clear origin or purpose.

            I know video submissions are not as attractive as articles, but I highly encourage you to check this one out.

            1. 1

              I haven’t watched the video yet, but I’ve saved it in my Watch Later list.

              Another video that I liked regarding FFT - https://www.youtube.com/watch?v=spUNpyF58BY

              1. 1

                Ah, I’ve seen this one. Always good stuff from 3blue1brown. Though that’s about the Fourier transform in general, from a mathematical perspective.

            1. 5

              I feel pretty lucky that from very early on we were pretty far from this at $WORK. But we do still have “operational stuff that gets pretty dangerous”, and it’s all kinda scary (like most toil honestly).

              One recent strategy has been to build runscripts based off “do-nothing scripts” (see this post).

              It establishes all the steps, allows for admonitions, and establishess ways to provide good automation.

              One thing that has been pretty nice is hooking this up with our cloud provider CLI tooling to allow for more targetted workflows (much more assurances that you are actually in prod or in staging etc), and then turning our “do-nothing script” to a proper runbook that just does the thing that needs to happen.

              One trick here for people who have dog-slow CI or the like, is to have this in a repo that is more ammenable to fast git merges. That + having a staging environment that is allowed to be broken temporarily gets rid of a lot of excuses. Along with giving people the space to actually do this kind of work!

              1. 2

                do-nothing scripts look awfully like checklists (which are a great idea!)

                1. 1

                  Yeah, but then they provide a way to automate some of the steps incrementally.

                2. 2

                  Thank you for showing me “do nothing scripts”. That’s a really interesting, actionable idea.

                  1. 1

                    If you have anything outside your own project that relies on the staging environment, you will also need some other environment that is not allowed to break.

                    Working as a front end developer against a staging environment that is always breaking is really bad for morale.

                  1. 3

                    This sshd got started inside the “doubly niced” environment

                    As for why “the processes didn’t notice and then undo the nice/ionice values”, think about it. Everyone assumes they’re going to get started at the usual baseline/default values. Nobody ever expects that they might get started down in the gutter and have to ratchet themselves back out of it. Why would they even think about that?

                    These days, this should stand out as a red flag – all these little scripts should be idempotent.

                    You shouldn’t write scripts where if you Ctrl-C them, and then re-run it, you’ll get these “doubling” effects.

                    Otherwise if the machine goes down in the middle, or you Ctrl-C, you are left with something that’s very expensive to clean up correctly. Writing Idempotent scripts avoids that – and that’s something that’s possible with shell but not necessarily easy.

                    As far as I can tell, idempotence captures all fhte benefits of being “declarative”. The script should specify the final state, not just a bunch of steps that start from some presumed state – which may or may not be the one you’re in!


                    I guess there is not a lot of good documentation about this, but here is one resource I found: https://arslan.io/2019/07/03/how-to-write-idempotent-bash-scripts/

                    Here’s another one: https://github.com/metaist/idempotent-bash

                    1. 9

                      I believe the “doubly niced” refers to “both ionice and nice”. There wasn’t any single thing being done twice by accident. The issue is with processes inheriting the settings due to Unix semantics.

                      1. 4

                        The problem is the API - it increments the nice value rather than setting it. From the man page:

                        The nice() function shall add the value of incr to the nice value of the calling process.

                        So the nice value did end up bigger than desired.

                        1. 3

                          That is an interesting quirk of nice()/renice, but in this case I believe they explicitly stated they originally set the nice value to 19, which is the maximum.

                          1. 2

                            Thanks, you’re right! Took me a second reading…

                        2. 1

                          Ah yeah you could be right …

                          But still the second quote talks about something related to idempotence. It talks about assuming you’re in a certain state, and then running a script, but you weren’t actually in that state. Idempotence addresses that problem. It basically means you will be in the same finishing state no matter what the starting state is. The state will be “fixed” rather than “mutated”.

                          1. 3

                            Hmm, I still don’t think this is the case. The state being dealt with is entirely implicit, and the script in question doesn’t do anything with nice values at all, and yet still should be concerned about them.

                      1. 26

                        I find the complaints about Go sort of tedious. What is the difference between using go vet to statically catch errors and using the compiler to statically catch errors? For some reason, the author finds the first unacceptable but the second laudable, but practically speaking, why would I care? I write Go programs by stubbing stuff to the point that I can write a test, and then the tests automatically invoke both the compiler and go vet. Whether an error is caught by the one or the other is of theoretical interest only.

                        Also, the premise of the article is that the compiler rejecting programs is good, but then the author complains that the compiler rejects programs that confuse uint64 with int.

                        In general, the article is good and informative, but the anti-Go commentary is pretty tedious. The author is actually fairly kind to JavaScript (which is good!), but doesn’t have the same sense of “these design decisions make sense for a particular niche” when it comes to Go.

                        1. 35

                          What is the difference between using go vet to statically catch errors and using the compiler to statically catch errors?

                          A big part of our recommendation of Rust over modern C++ for security boiled down to one simple thing: it is incredibly easy to persuade developers to not commit (or, failing that, to quickly revert) code that does not compile. It is much harder to persuade them to not commit code where static analysis tooling tells them is wrong. It’s easy for a programmer to say ‘this is a false positive, I’m just going to silence the warning’, it’s very difficult to patch the compiler to accept code that doesn’t type check.

                          1. 34

                            What is the difference between using go vet to statically catch errors and using the compiler to statically catch errors?

                            One is optional, the other one is in your face. It’s similar to C situation. You have asan, ubsan, valgrind, fuzzers, libcheck, pvs and many other things which raise the quality is C code significantly when used on every compilation or even commit. Yet, if I choose a C project at random, I’d bet none of those are used. We’ll be lucky if there are any tests as well.

                            Being an optional addition that you need to spend time to engage with makes a huge difference in how often the tool is used. Even if it’s just one command.

                            (According to the docs only a subset of the vet suite is used when running “go test”, not all of them - “high-confidence subset”)

                            1. 15

                              When go vet automatically runs on go test, it’s hard to call it optional. I don’t even know how to turn if off unless I dig into the documentation, and I’ve been doing Go for 12+ years now. Technically gofmt is optional too, yet it’s as pervasive as it can be in the Go ecosystem. Tooling ergonomics and conventions matter, as well as first party (go vet) vs 3rd party tooling (valgrind).

                              1. 21

                                That means people who don’t have tests need to run it explicitly. I know we should have tests - but many projects don’t and that means they have to run vet explicitly and in practice they just miss out on the warnings.

                                1. 2

                                  Even in projects where I don’t have tests, I still run go test ./... when I want to check if the code compiles. If I used go build I would have an executable that I would need to throw away. Being lazy, I do go test instead.

                              2. 13

                                Separating the vet checks from the compilation procedure exempts those checks from Go’s compatibility promise, so they could evolve over time without breaking compilation of existing code. New vet checks have been introduced in almost every Go release.

                                Compiler warnings are handy when you’re compiling a program on your own computer. But when you’re developing a more complex project, the compilation is more likely to happen in a remote CI environment and making sure that all the warnings are bubbled up is tedious and in practice usually overlooked. It is thus much simpler to just have separate workflows for compilation and (optional) checks. With compiler warnings you can certainly have a workflow that does -Werror; but once you treat CI to be as important as local development, the separate-workflow design is the simpler one - especially considering that most checks don’t need to perform a full compilation and is much faster that way.

                                Being an optional addition that you need to spend time to engage with makes a huge difference in how often the tool is used. Even if it’s just one command.

                                I feel that the Go team cares more about enabling organizational processes, rather than encouraging individual habits. The norm for well-run Go projects is definitely to have vet checks (and likely more optional linting, like staticcheck) as part of CI, so that’s perhaps good enough (for the Go team).

                                All of this is quite consistent with Go’s design goal of facilitating maintenance of large codebases.

                                1. 5

                                  Subjecting warnings to compatibility guarantees is something that C is coming to regret (prior discussion).

                                  And for a language with as… let’s politely call it opinionated a stance as Go, it feels a bit odd to take the approach of “oh yeah, tons of unsafe things you shouldn’t do, oh well, up to you to figure out how to catch them and if you don’t we’ll just say it was your fault for running your project badly”.

                                2. 4

                                  The difference is one language brings the auditing into the tooling. In C, it’s all strapped on from outside.

                                  1. 19

                                    Yeah, “similar” is doing some heavy lifting there. The scale is more like: default - included - separate - missing. But I stand by my position - Rust is more to the left the than Go and that’s a better place to be. The less friction, the more likely people will notice/fix issues.

                                  2. 2

                                    I’ll be honest, I get this complaint about it being an extra command to run, but I haven’t ever run go vet explicitly because I use gopls. Maybe I’m in a small subset going the LSP route, but as far as I can tell gopls by default has good overlap with go vet.

                                    But I tend to use LSPs whenever they’re available for the language I’m using. I’ve been pretty impressed with rust-analyzer too.

                                  3. 12

                                    On the thing about maps not being goroutine safe, it would be weird for the spec to specify that maps are unsafe. Everything is unsafe except for channels, mutxes, and atomics. It’s the TL;DR at the top of the memory model: https://go.dev/ref/mem

                                    1. 6

                                      Agreed. Whenever people complain about the Rust community being toxic, this author is who I think they’re referring to. These posts are flame bait and do a disservice to the Rust community. They’re like the tabloid news of programming, focusing on the titillating bits that inflame division.

                                      1. 5

                                        I don’t know if I would use the word “toxic” which is very loaded, but just to complain a little more :-) this passage:

                                          go log.Println(http.ListenAndServe("localhost:6060", nil))
                                        

                                        Jeeze, I keep making so many mistakes with such a simple language, I must really be dense or something.

                                        Let’s see… ah! We have to wrap it all in a closure, otherwise it waits for http.ListenAndServe to return, so it can then spawn log.Println on its own goroutine.

                                         go func() {
                                             log.Println(http.ListenAndServe("localhost:6060", nil))
                                         }()
                                        

                                        There are approximately 10,000 things in Rust that are subtler than this. Yes, it’s an easy mistake to make as a newcomer to Go. No, it doesn’t reflect even the slightest shortcoming in the language. It’s a very simple design: the go statement takes a function and its arguments. The arguments are evaluated in the current gorountine. Once evaluated, a new goroutine is created with the evaluated parameters passed into the function. Yes, that is slightly subtler than just evaluating the whole line in a new goroutine, but if you think about it for one second, you realize that evaluating the whole line in a new goroutine would be a race condition nightmare and no one would actually want it to work like that.

                                        Like, I get it, it sucks that you made this mistake when you were working in a language you don’t normally use, but there’s no need for sarcasm or negativity. This is in fact a very “simple” design, and you just made a mistake because even simple things actually need to be learned before you can do them correctly.

                                        1. 3

                                          In practice, about 99% of uses of the go keyword are in the form go func() {}(). Maybe we should optimize for the more common case?

                                          1. 1

                                            I did a search of my code repo, and it was ⅔ go func() {}(), so you’re right that it’s the common case, but it’s not the 99% case.

                                          2. 2

                                            I agree that the article’s tone isn’t helpful. (Also, many of the things that the author finds questionable in Go can also be found in many other languages, so why pick on Go specifically?)

                                            But could you elaborate on this?

                                            evaluating the whole line in a new goroutine would be a race condition nightmare and no one would actually want it to work like that.

                                            IMO this is less surprising than what Go does. The beautiful thing about “the evaluation of the whole expression is deferred” is precisely that you don’t need to remember a more complicated arbitrary rule for deciding which subexpressions are deferred (all of them are!), and you don’t need ugly tricks like wrapping the whole expression in a closure which is the applied to the empty argument list.

                                            Go’s design makes sense in context, though. Go’s authors are culturally C programmers. In idiomatic C code, you don’t nest function calls within a single expression. Instead, you store the results of function calls into temporary variables and only then pass those variables to the next function call. Go’s design doesn’t cause problems if you don’t nest function calls.

                                        2. 3

                                          At least they mention go vet so even people like me without knowing it can arrive at similar conclusions. And they also mention that he is somewhat biased.

                                          But I think they should just calmly state without ceremony like “And yet there are no compiler warnings” that this is the compiler output and this is the output of go vet.

                                          This also seems unnecessary:

                                          Why we need to move it into a separate package to make that happen, or why the visibility of symbols is tied to the casing of their identifiers… your guess is as good as mine.

                                          Subjectively, this reads as unnecessarily dismissive. There are more instances similar to this, so I get why you are annoyed. It makes their often valid criticism weaker.

                                          I think it comes as a reaction to people valid agreeing that golang is so simple but in their (biased but true) experience it is full of little traps.

                                          Somewhat related: What I also dislike is that they use loops for creating the tasks in golang, discuss a resulting problem and then not use loops in rust - probably to keep the code simple

                                          All in all, it is a good article though and mostly not ranty. I think we are setting the bar for fairness pretty high. I mean we are talking about a language fan…

                                          1. 5

                                            This also seems unnecessary: […]

                                            Agree. The frustrating thing here is that there are cases where Rust does something not obvious, the response is “If we look at the docs, we find the rationale: …” but when Go does something that is not obvious, “your guess is as good as mine.” Doesn’t feel like a very generous take.

                                            1. 6

                                              the author has years of Go experience. He doesn’t want to be generous, he has an axe to grind.

                                              1. 3

                                                So where’s the relevant docs for why

                                                we need to move it into a separate package to make that happen

                                                or

                                                the visibility of symbols is tied to the casing of their identifiers

                                                1. 3

                                                  we need to move it into a separate package to make that happen

                                                  This is simply not true. I’m not sure why the author claims it is.

                                                  the visibility of symbols is tied to the casing of their identifiers

                                                  This is Go fundamental knowledge.

                                                  1. 3

                                                    This is Go fundamental knowledge.

                                                    Yes, I’m talking about the rationale.

                                                    1. 3

                                                      https://go.dev/tour/basics/3

                                                      In Go, a name is exported if it begins with a capital letter.

                                                      1. 1

                                                        rationale, n.
                                                        a set of reasons or a logical basis for a course of action or belief

                                                      2. 2

                                                        Why func and not fn? Why are declarations var type identifier and not var identifier type? It’s just a design decision, I think.

                                                2. 1

                                                  The information is useful but the tone is unhelpful. The difference in what’s checked/checkable and what’s not is an important difference between these platforms – as is the level of integration of the correctness guarantees are with the language definition. Although a static analysis tool for JavaScript could, theoretically, find all the bugs that rustc does, this is not really how things play out. The article demonstrates bugs which go vet can not find which are precluded by Rust’s language definition – that is real and substantive information.

                                                  There is more to Go than just some design decisions that make sense for a particular niche. It has a peculiar, iconoclastic design. There are Go evangelists who, much more strenuously than this author and with much less foundation, criticize JavaScript, Python, Rust, &c, as not really good for anything. The author is too keen to poke fun at the Go design and philosophy; but the examples stand on their own.

                                                1. 4

                                                  I wonder if there’s any mechanism envisioned by the lawmakers allowing us to be sure that the data that “must be deleted” actually has. Apart from assurances from the guilty parties, that is. The cynic in me expects them to say that these data cannot be distinguished from the “lawfully” collected data, and they can’t be compelled to delete all of it.

                                                  1. 5

                                                    mechanism envisioned by the lawmakers

                                                    😅

                                                    1. 3

                                                      That would potentially put them in violation of https://gdpr-info.eu/recitals/no-42/ and likely into even more trouble. Mind you, the ruling already finds them in breach of https://gdpr-info.eu/art-30-gdpr/ for insufficient record-keeping.

                                                      1. 2

                                                        Actually, more importantly, there is no mechanism to delete this data because there is no way that there is consent attribution that captures where the consent came from and all the downstream data that can be attributed to it. I don’t see how these companies can delete this data. Unless they just delete all user accounts (and all associated data) that came into contact with these popups.

                                                        1. 8

                                                          That is a strawman. There’s a pretty clear difference between data the user entered themselves and data obtained by the system through tracking, for advertising purposes.

                                                        2. 1

                                                          Of course there is an audit process in place.

                                                          Any company that works with personally identifiable information supposed to appoint a Data Protection Officer, whose responsibility is to ensure a GDPR compliance and to interface with a data protection authority on behalf of the company. This person is not liable for the GDPR breaches, but IS personally responsible for reporting organizations failures to comply with regulations (to the best of their knowledge of course).

                                                          Sure, it’s always possible to cheat the system, but the bigger the company the harder it would be to keep such conspiracy a secret.

                                                          Surprisingly, the system works pretty well it seems. Just in 2021 there have been major fines issued to, among others, the usual suspects Amazon, Google and Facebook. Sure those cases will go through the obligatory appeal process but those are (fortunately) rarely successful, since the GDPR regulations at this point are generally well understood.

                                                          1. 3

                                                            Sure, it’s always possible to cheat the system, but the bigger the company the harder it would be to keep such conspiracy a secret.

                                                            While it’s true, also the bigger the company, the easier it is to have an accidental copy of some data which is not hooked up to the cleanup system. Not even out of malice.

                                                            While I expect Google and others to actually try to keep the pii secure and isolated, there’s going to be lots of other pieces about users which just end up too distributed.

                                                            1. 3

                                                              Interestingly enough this is also somewhat addressed in GDPR. Data should only be in places it is actually required for business purposes and can’t be just transferred „just in case“ or something. Furthermore, locations and reasons for data processing should be documented by DPO. Not that that’s bulletproof, but it’s not naive at least.

                                                              1. 2

                                                                I believe that companies actually care and try to keep the data distribution under control. But as you say it’s not bulletproof. I’ve seen silly and unexpected chains of events like: object with user data gets default string serialisation used by error reporter as part of message, which saves the info, which gets collated into a separate database for analysis. And that’s one of the more obvious problems.

                                                              2. 2

                                                                We’re 3 years into GDPR, no more excuses. With that amount of money and power, any negligence is to be considered malice.

                                                                1. 1

                                                                  That’s not a GDPR-related excuse. It’s a reality of massive projects. In the same way we know things are not 100% reliable and work around it as needed, storage will have some exceptions where something got cached somewhere that you don’t have in your cleanup procedure.

                                                                  1. 3

                                                                    If an automated train or plane has a critical failure and kills people, the reaction we have is not “well it’s a reality of massive projects”; the manufacturers of the involved systems will have to spend a lot of effort fixing their issues, and fixing their processes so that the same issue does not occur again. These requirements have costs (in particular they increase the cost of producing software greatly), which is commensurate to the values that we decided, as a society, to give to human lives.

                                                                    GDPR is not a “critical system” in the same sense that human lives are immediately in danger, I’m not trying to say that the exact same approach should be followed. But it’s on the same scale: how much do we value privacy and user protection? Europe has ruled that it values it seriously, and has put laws in place (and enforcement procedures) to ensure that people implementing systems that deal with personal information do it very carefully, in a different way that other sort of data is handled. “We know that things are not 100% reliable” is not an excuse in itself (as it could be in a project with no correctness requirements, or very weak expectations of quality); you have to prove that you took appropriate care, commensurate with the value of the data.

                                                                    1. 1

                                                                      See how quickly that excuse liquifies under the pressure of a daily non compliance penalty…

                                                            1. 2

                                                              What’s interesting about the ui? Simply that it’s vector based?

                                                              1. 13

                                                                I also find interesting the tabbed windows – each tab can be a different app

                                                                1. 5

                                                                  Like Haiku!

                                                                  1. 2

                                                                    Fluxbox also offers that.

                                                                2. 2

                                                                  If we’re raising questions, what’s with boots in seconds, don’t all OSes do?

                                                                  Edit: not that this doesn’t look interesting, it’s just that that particular boast caught my eye.

                                                                  1. 18

                                                                    There’s a great Wiki Page for FreeBSD that Colin Percival (of tarsnap fame) has been maintaining on improving FreeBSD boot time. In particular, this tells you where the time goes.

                                                                    A lot of the delays come from things that are added to support new hardware or simply from the size of the code. For example, loading the kernel takes 260ms, which is a significant fraction of the 700ms that Essence takes. Apple does (did?) a trick here where did a small amount of defragmentation of the filesystem to ensure that the kernel and everything needed for boot were contiguous on the disk and so could be streamed quickly. You can also address it by making the kernel more modular and loading components on demand (e.g. with kernel modules), but that then adds latency later.

                                                                    Some of the big delays (>1s) came from sleep loops that wait for things to stabilise. If you’re primarily working on your OS in a VM, or on decent hardware, then you don’t need these delays but when you start deploying on cheap commodity hardware then you discover that a lot of devices take longer to initialise than you’d expect. A bunch of these things were added in the old ISA days and so may well be much too long. Some of them are still necessary for big SCSI systems (a big hardware RAID array may take 10s of seconds to become available to the OS).

                                                                    Once the kernel has loaded, there’s the init system. This is something that launchd, SMF, and systemd are fairly good at. In general, you want something that can build a dynamic dependency graph and launch things as their dependencies are fulfilled but you also need to avoid thundering herds (if you launch all of the services at once then you’ll often suffer more from contention than you’ll gain from parallelism).

                                                                    On top of that, on *NIX platforms, there’s then the windowing system and DE. Launching X.org is fairly quick these days but things like KDE and GNOME also bundle a load of OS-like functionality. They have their own event framework and process launchers (I think systemd might be subsuming some of this on Linux?) and so have the same problem of starting all of the running programs.

                                                                    The last bit is something that macOS does very well because they cheat. The window server owns the buffer that contains every rendered window and persists this across reboot. When you log back in, it displays all of your apps’ windows in the same positions that they were, with the same contents. If then starts loading them in the background, sorted by the order in which you try to run them. Your foreground app will be started first and so the system typically has at least a few seconds of looking at that before you focus on anything else and so it can hide the latency there.

                                                                    All of that said, for a desktop OS, the thing I care about the most is not boot time, it’s reboot time. How long does it take between shutting down and being back in exact same state in all of my apps that I was in before the reboot? If I need a security update in the kernel or a library that’s linked by everything, then I want to store all state (including window positions and my position within all open documents, apply the update, shut down, restart, reload all of the state, and continue working. Somewhat related, if the system crashes, how long does it take me to resume from my previous state? Most modern macOS apps are constantly saving restore points to disk and so if my Mac crashes then it typically takes under a minute to get back to where I was before the reboot. This means I don’t mind installing security updates and I’m much more tolerant of crashes than on any other system (which isn’t a great incentive for Apple’s CoreOS team).

                                                                    1. 1

                                                                      And essence basically skips all of that cruft? Again, not to be putting the project down, but all that for a few seconds doesn’t seem much, once a week.

                                                                      I don’t think I reboot my Linux boxes more often, and even my work Windows sometimes reminds me that I must reboot once a week because if company policy.

                                                                      Maybe if I had an old slow laptop it would matter to me more. Or of i was doing something with low-power devices (but then, I would probably be using something more specialised there, if that was important).

                                                                      Again. Impressive feat. And good work and I hope they make something out of it (in the long run, I mean). But doesn’t Google also work on fuchsia, and Apple on macos? They probably have much more chance to become new desktop leaders. I don’t know, this seems nice but I think there biggest benefit is in what the authors will learn from the project and apply elsewhere.

                                                                      1. 2

                                                                        And essence basically skips all of that cruft? Again, not to be putting the project down, but all that for a few seconds doesn’t seem much, once a week.

                                                                        It probably benefits from both being small (which it gets for free by being new) and from not having been tested much on the kind of awkward hardware that requires annoying spin loops. Whether they can maintain this is somewhat open but it’s almost certainly easier to design a system for new hardware that boots faster than it is to design a system for early ’90s hardware, refactor it periodically for 30 years, and have it booting quickly.

                                                                        But doesn’t Google also work on fuchsia, and Apple on macos? They probably have much more chance to become new desktop leaders. I don’t know, this seems nice but I think there biggest benefit is in what the authors will learn from the project and apply elsewhere.

                                                                        I haven’t paid attention to what Fuchsia does for userspace frameworks (other than to notice that Flutter exists). Apple spent a lot of effort on making this kind of thing fast but most of it isn’t really to do with the kernel. Sudden Termination came from iOS but is now part of macOS. At the OS level, apps enter a state where they have no unsaved state and the kernel will kill them (equivalent of kill -9) whenever it wants to free up memory. The WindowServer keeps their window state around so that they can be restored in the background. This mechanism was originally so iOS could kill background apps instead of swapping but it turns out to be generally useful. The OS parts are fairly simple, extending Cocoa so that it’s easy to write apps that respect this rule was a lot more difficult work.

                                                                    2. 5

                                                                      In the demo video, it booted in 0.7s, which, to me, is impressive. Starting applications and everything is very snappy too. The wording of the claim doesn’t do it justice though, I agree with that.

                                                                      1. 3

                                                                        Ideally you should almost never have to reboot an OS, so boot time doesn’t interest me nearly as much as good power management (sleep/wake).

                                                                        1. 3

                                                                          how many people live in this ideal world where you never have to reboot the OS?

                                                                          1. 6

                                                                            IBM mainframe operators.

                                                                            1. 4

                                                                              It’s not never, but I basically only reboot my macs and i(pad)os devices for OS updates, which is a handful of times per year. The update itself takes long enough that the reboot time part of it is irrelevant - I go something else while the update is running.

                                                                              1. 3

                                                                                I think it’s only really Windows that gets rebooted. I used to run Linux and OpenBSD without reboots for years sometimes, and like you I only reboot MacOS when I accidentally run out of laptop battery or do an OS update, as you say.

                                                                              2. 3

                                                                                I dunno; how many people own Apple devices? I pretty much only reboot my Macs for OS updates, or the rare times I have to install a driver. My iOS devices only reboot for updates or if I accidentally let the battery run all the way down.

                                                                                I didn’t think this was a controversial statement, honestly. Haven’t Windows and Linux figured out power management by now too?

                                                                                1. 1

                                                                                  pretty much only reboot my Macs for OS updates, or the rare times I have to install a driver

                                                                                  That’s not “never”, or are MacOS updates really so far/few between?

                                                                                2. 1

                                                                                  I feel like this is one of those things where people are still hung up from the days of slow HDDs and older versions of Windows bloated with all kinds of software on startup.

                                                                                  1. 1

                                                                                    It depends a bit on the use case. For client devices, I agree, boot time doesn’t matter nearly as much as resume speed and application relaunch speed. For cloud deployments, it can matter a lot. If you’re spinning up a VM instance for each CI job, for example, then anything over a second or two starts to be noticeable in your total CI latency.

                                                                                3. 2

                                                                                  If it boots fast, does sleep matter?

                                                                                  1. 6

                                                                                    It does unless you can perfectly save state each time you boot. And boot in less than a second.

                                                                                    1. 4

                                                                                      Only if it can somehow store the entire working state, including unsaved changes, and restore it on boot. Since that usually involves relaunching a bunch of apps, it takes significantly longer than a simple boot-to-login-screen.

                                                                                      This isn’t theoretical. Don’t you have any devices that sleep/wake reliably and quickly? It’s profoundly better than having to shut down and reboot.

                                                                                      1. 2

                                                                                        Only if it can somehow store the entire working state, including unsaved changes, and restore it on boot

                                                                                        That’s another interesting piece of the design space. I’ve seen research prototypes on Linux and FreeBSD (I think the Linux version maybe got merged?) that extend the core dump functionality to provide a complete dump of memory and associated kernel state (open file descriptors). Equivalent mechanisms have been around in hypervisors for ages because they’re required for suspend / resume and migration. They’re much easier in a hypervisor because they interfaces for guests have a lot less state: a block device has in-flight transactions, a network device has in-flight packets, and all other state (e.g. TCP/IP protocol state, file offsets) is stored in the guest. For POSIXy systems, various things are increasingly difficult:

                                                                                        • Filesystem things are moderately easy. You need to store the inode and offset. If another process modifies the file while you’re suspended then it’s not really different than another process modifying it while you’re running. Filesystem locks are a bit more interesting - if a process holds a filesystem lock and is suspended to disk, what should happen? You probably don’t want to leave the file locked until the process is reloaded, because it might not be. On the other hand, it will probably break in exciting ways if it silently drops the lock across suspend / resume. This isn’t a problem if you’re suspending / resuming all processes at the same time.
                                                                                        • Network connections are basically impossible, which makes them easy: you just drop all connections and restore listening / bound sockets. Most programs already know how to handle the network going away intermittently.
                                                                                        • Local IPC can be interesting. If I create a pipe and fork, then one of the children is frozen to disk, what should happen? If both are frozen and restored together, ideally they’d both get the pipe back in the same state, which means that I need to persist a UUID or similar for each IPC connection so that restoring groups of processes (e.g. a window server and an application) can work.

                                                                                        If you have this mechanism and you have fast reboot, then you don’t necessarily need OS sleep states. If you also have a sudden termination mechanism then you can use this as fallback for apps that aren’t in sudden-termination state.

                                                                                        Of course, it depends a bit on why people are rebooting. Most of the time I reboot, it’s to install a security update. This is more likely to be in a userspace library than the kernel. As a user, the thing I care most about is how quickly I can restart my applications and have them resume in the same state. If the kernel / windowing system can restart in <1s that’s fine, but if my apps lose all of their state across a restart then it’s annoying. Apple has done a phenomenal amount of work over the last decade to make losing state across app restarts unusual (including work in the frameworks to make it unusual for third-party apps).

                                                                                        1. 1

                                                                                          All my devices can sleep/wake fine, but I almost never use it. My common apps all auto start on boot and with my SSDs I boot in a second or two (so same as time to come out of sleep honestly, in both cases the slowest part is typing my password).

                                                                                          1. 1

                                                                                            On my current laptop, it wakes up instantly when I open the lid, enter the password, and the state is as exactly as I left it. (And it’s probably less gigabytes written to disk than hibernation either.)

                                                                                1. 30

                                                                                  Re: https://github.com/github/markup/issues/533

                                                                                  I’m the main author of KeenWrite (see screenshots), a type of desktop Markdown editor that supports diagrams. It’s encouraging to see that Mermaid diagrams are being supported in GitHub. There are a few drawbacks on the syntax and implications of using MermaidJS.

                                                                                  First, only browser-based SVG renderers can correctly parse Mermaid diagrams. I’ve tested Apache Batik, svgSalamander, resvg, rsvg-convert, svglib, CairoSVG, ConTeXt, and QtSVG. See issue 2485. This implies that typesetting Mermaid diagrams is not currently possible. In effect, by including Mermaid diagrams, many documents will be restricted to web-based output, excluding the possibility of producing PDF documents based on GitHub markdown documents (for the foreseeable future).

                                                                                  Second, there are numerous text-to-diagram facilities available beyond Mermaid. The server at https://kroki.io/ supports Mermaid, PlantUML, Graphviz, byte fields, and many more. While including MermaidJS is a great step forward, supporting Kroki diagrams would allow a much greater variety. (Most diagrams produced in MermaidJS can also be crafted in Graphviz, albeit with less terse syntax.)

                                                                                  Third, see the CommonMark discussion thread referring to a syntax for diagrams. It’s unfortunate that a standard “namespace” concept was not proposed.

                                                                                  Fourth, KeenWrite integrates Kroki. To do so, it uses a variation on the syntax:

                                                                                  ``` diagram-mermaid
                                                                                  ```
                                                                                  
                                                                                  ``` diagram-graphviz
                                                                                  ```
                                                                                  
                                                                                  ``` diagram-plantuml
                                                                                  ```
                                                                                  

                                                                                  The diagram- prefix tells KeenWrite that the content is a diagram. The prefix is necessary to allow using any diagram supported by a Kroki server without having to hard-code the supported diagram type within KeenWrite. Otherwise, there is no simple way to allow a user to mark up a code block with their own text style that may coincide with an existing diagram type name.

                                                                                  Fifth, if ever someone wants to invent a programming language named Mermaid (see MeLa), then it precludes the possibility of using the following de facto syntax highlighting:

                                                                                  ``` mermaid
                                                                                  ```
                                                                                  

                                                                                  My feature request is to add support for Kroki and the diagram- prefix syntax. That is:

                                                                                  ``` diagram-mermaid
                                                                                  ```
                                                                                  

                                                                                  And deprecate the following syntax:

                                                                                  ``` mermaid
                                                                                  ```
                                                                                  

                                                                                  And, later, introduce the language- prefix for defining code blocks that highlight syntax. That is, further deprecate:

                                                                                  ``` java
                                                                                  ```
                                                                                  

                                                                                  With the following:

                                                                                  ``` language-java
                                                                                  ```
                                                                                  

                                                                                  That would provide a “namespace” of sorts to avoid naming conflicts in the future.

                                                                                  1. 10

                                                                                    I don’t think moving the existing stuff to language- is necessary, however I agree that diagram-mermaid is a better option – especially if one wants syntax highlighting for the syntax of the Mermaid diagramming language, to describe how to write such diagrams.

                                                                                    1. 1

                                                                                      First, only browser-based SVG renderers can correctly parse Mermaid diagrams. I’ve tested Apache Batik, svgSalamander, resvg, rsvg-convert, svglib, CairoSVG, ConTeXt, and QtSVG. See issue 2485

                                                                                      Do you mean the output of mermaid.js? Besides that these SVG parsers should be fixed if they are broken and maybe mermaid.js could get a workaround, surely a typset system could read the mermaid syntax directly and not the output of a for-web implementation of it?

                                                                                      1. 2

                                                                                        If you look at the issue, there’s a fairly extensive list of renderers affected. This suggests that the core problem is that mermaid uses some feature(s) which are not widely supported.

                                                                                        1. 1

                                                                                          Besides that these SVG parsers should be fixed if they are broken

                                                                                          Not sure if they are broken per se. The EchoSVG project aims to support custom properties, which would give it the ability to render Mermaid diagrams. From that thread, you can see supporting SVG diagrams that use custom properties is no small effort. Multiply that effort by all the renderers listed and we’re probably looking at around ten years’ worth of developer hours.

                                                                                          surely a typset system could read the mermaid syntax directly and not the output of a for-web implementation of it

                                                                                          Yes. It’s not for free, though. Graphviz generates graphs on par with the complexity of Mermaid graphs and its output can be rendered with all software libraries I tried. IMO, changing Mermaid to avoid custom properties would take far less effort than developing custom property renderers at least eight times over.

                                                                                          1. 2

                                                                                            IMO, changing Mermaid to avoid custom properties would take far less effort than developing custom property renderers at least eight times over.

                                                                                            Sure, but as I said the ideal would be neither of those, but to just typeset the mermaid syntax directly and not rely on the JS or the SVG at all.

                                                                                      1. 2

                                                                                        Interesting, what do you mean by this is a better compromise for scripts? I’m not sure I see where this would be much different in that context.

                                                                                        1. 2

                                                                                          I’m working on a deployment tool https://deployer.org/ and for example, if you want to use git and clone repo for the first time (from example from CI) you need to manually login into the server and run the ssh command to github.com to update knopwn_hosts.

                                                                                          With accept-new this workflow is automated and no manual setup is needed.

                                                                                          1. 1

                                                                                            I imagine it’ll be better for scripts that issue multiple SSH commands. You can verify the remote end hasn’t changed host keys between the two (or more) invocations of SSH; whereas with no you just accept whatever the host key is whether it changes or not.

                                                                                            You can’t tell if the host changes between script runs but you can be sure the host hasn’t changed during the current run.

                                                                                            1. 4

                                                                                              I solve this in CI by putting the host’s fingerprint in a variable and writing that to known_hosts. I would think the odds of a host key changing in between commands of a job would be tiny, and the damage could already be done.

                                                                                              It’s still “trust on first use”, but that first use is when I set up CI and set the variable, not at the start of every job.

                                                                                              1. 3

                                                                                                I think this is the correct way to do it, I do this as well for CI jobs SSH-ing to longer-lived systems.

                                                                                                If the thing I’m SSHing into is ephemeral, I’ll make it upload its ssh host public keys to an object storage bucket when it boots via its cloud-init or “Userdata” script. That way the CI job can simply look up the appropriate host keys in the object storage bucket.

                                                                                                IMO any sort of system that creates and destroys servers regularly, like virtual machines or VPSes, should make it easy to query or grab the machine’s ssh public keys over something like HTTPS, like my object storage bucket solution.

                                                                                                I guess this is a sort of pet peeve of mine. I was always bugged by the way that Terraform’s remote-exec provisioner turns off host key checking by default, and doesn’t warn the user about that. I told them this is a security issue and they told me to buzz off. Ugh. I know its a bit pedantic, but I always want to make sure I have the correct host key before I connect!!! Similar to TLS, the entire security model of the connection can fall apart if the host key is not known to be authentic.

                                                                                              2. 2

                                                                                                Unless you’re clearing the known_hosts file (and if so, WTF), I don’t see why there would be a difference between consecutive connections within a script and consecutive connections between script runs.

                                                                                                1. 4

                                                                                                  Jobs/tasks running under CI pipelines often don’t start with a populated known_hosts. Ephemeral containers too. Knowing you’re still talking to the same remote end (or someone with control of the same private key at least) is better than just accepting any remote candidate in that case.

                                                                                                  Less “clearing known_hosts” file, more “starting without a known_hosts” file.

                                                                                            1. 2

                                                                                              As much as I like Z3, I don’t think it is the right tool for this problem. I’d be willing to bet that encoding the dictionary into the solver will make it simply check each word separately, and you can probably do that faster and more legibly by iterating over the wordlist manually and checking the constraints like that.

                                                                                              Case in point, the many different constraints implementations shown don’t even cover the full range of possibilities you can encounter. Is that perhaps because it is hard to think about the general solution?

                                                                                              1. 2

                                                                                                I don’t think the point of this article is to say that Z3 is the right tool for this job, but demonstrate how you might solve a tangible problem using it.

                                                                                              1. 1

                                                                                                You could have .into_enum() be part of the trait. That way you don’t have to worry about non-first-class implementations.

                                                                                                1. 3

                                                                                                  I scrolled down to the conclusion section hoping to learn about why it is slow in some quick words. But there was none :/ Any TLDR folks?

                                                                                                  1. 12

                                                                                                    In this case, it is because of known compile time regression in Rust 1.57.0 which will be fixed in 1.58.0. Compared to methods, the answer itself is rather unenlightening.

                                                                                                    1. 6

                                                                                                      Yeah, in this case it’s more about the journey taken to figure it out.

                                                                                                    2. 4

                                                                                                      TL;DR: There was a giant generic type that took forever for the compiler to handle. That type came from a web server library called “warp”, which is famous for its extreme use of generics and playing games with the type system. The fix was to use dynamic dispatch instead of monomorphization, which erases the type so the compiler doesn’t have to keep track of it. If that sounds hard, it’s not. It’s literally just one method on the end of the normal type called “boxed”.

                                                                                                    1. 3

                                                                                                      That story is hilarious. That anyone would have gone down the path to implement this functionality without knowing about what DLLs do….

                                                                                                      Having said that, I’ve copied code using memcpy() in the past. This was on a 32-bit ARM platform, for re-programming the flash memory of the main program from a bootloader. This was necessary because you couldn’t access (or execute code out of) a region of flash memory when programming it, even if you weren’t erasing the sector or bank that had the bootloader code in it. So we went through the whole process of looking through the generated assembly to make sure it was OK. We didn’t use anything on the stack, or even local variables, instead hardcoding absolute memory addresses for vars.

                                                                                                      1. 1

                                                                                                        I suppose instead of reviewing the assembly, one could use a separate link section, such that you can specify the load address in the linker script.

                                                                                                      1. 2

                                                                                                        Anything that gets the computer checking the checksum for you is a step up in my book! Relatedly, I did a roundup a couple of years ago of minimal techniques for verifying checksums without having to eyeball them manually. If anyone knows any better ones I’d love to hear them.

                                                                                                        1. 2

                                                                                                          My solution is very low-tech: copy the hash from the terminal, and in the browser, Ctrl+F Ctrl+V. If it highlights the hash on the website, you’re good.

                                                                                                        1. 20

                                                                                                          Formal methods. I’ve already committed to this since I convinced my team lead that it’s be a good idea to specify our system in TLA+, so I’m gonna read up on it during the holidays and hopefully not prove myself wrong.

                                                                                                          Prolog, wanted to do a web application with its http library and use it as database.

                                                                                                          Some hardware stuff maybe. My BU at work does a lot of hardware/embedded stuff and I’d love to learn how some of it works.

                                                                                                          Reading/writing assembly, so spending a lot of time on Compiler Explorer probably.

                                                                                                          1. 5

                                                                                                            Prolog, wanted to do a web application with its http library and use it as database.

                                                                                                            I’m curious why you’re interested in Prolog. When I was taught Prolog, it was as an example of a category of programming languages that doesn’t really exist. I’ve actually written a non-trivial amount of Prolog (and enjoy it), but the languages that inherit ideas from Prolog tend to be proof assistants and solvers, rather than general purpose languages. SMT solvers such as Z3 are the closest to descendants of Prolog and are a lot more generally useful (Prolog has SLD derivation and cuts to hack it to try to explore the solution space in other directions, most solvers have pluggable tactics). If I were starting today, I’d learn Z3 rather than Prolog.

                                                                                                            1. 2

                                                                                                              Well first of all, Z3 doesn’t really fit my purpose of writing a web application, and my plan was more to write a web application and learn Prolog through the process rather than learning Prolog by itself. I’m admittedly more interested in getting the program done than learn everything about Prolog.

                                                                                                              Second, I don’t really know what I could use Z3 for, or rather, I don’t know what it does exactly and I haven’t found a project that interests me where I think it could be useful. Maybe somebody else could enlighten me on this.

                                                                                                              1. 2

                                                                                                                Z3 is an example of an SMT solver. Those take a set of constraints as input, and try to either return an example set of values that satisfy the constraints, or prove that it’s impossible.

                                                                                                              2. 1

                                                                                                                SMT solvers such as Z3 are the closest to descendants of Prolog

                                                                                                                I’d consider Answer Set Programming (ASP) to be the closest descendant. Current practical implementations also have a “solver” flavor (like Z3) but the language uses close to Prolog syntax, and retains semantics that imo capture many of the interesting features of Prolog, like negation-as-failure, ability to straightforwardly define transitive closure, etc. (it comes out of attempts to come up with a less operational semantics for Prolog, of which one proposal, the “stable model semantics”, became the basis for ASP). I use clingo as the implementation, which is pretty solid.

                                                                                                              3. 4

                                                                                                                Plus one for learning TLA+ this year. I ordered @hwayne’s book a year or so ago and read it but didn’t complete all the exercises.

                                                                                                                I found the whole thing frustratingly almost made sense while remaining just out of reach. I had trouble imagining systems that were both motivating to try to model, and also small / simple enough that I would have a chance of succeeding. Systems that would be really helpful to model at work were just way too complicated for me, but problems that I felt I could probably get working seemed trivial and not interesting enough to motivate me to work on them.

                                                                                                                I’d be very interested if anyone had some suggestions for exercises or problems of various levels of difficulty to practice on. Something like exercism for TLA+ would be awesome.

                                                                                                                1. 1

                                                                                                                  I think our system is at a sweet spot where it’s not terribly complicated, but also very prone to missing edge cases, and there’s a few very clear invariants that should hold up all throughout, so I think mapping it to what (admittedly little) I know about TLA+ should be possible without too much pain. I’ll probably also try to write a blog post about it when I’m at a good point in specifying it.

                                                                                                                2. 2

                                                                                                                  TLA+ legitimately changed how I view software. That’s really the best case scenario when learning a new tool - it affects the way you think, whether or not you actually end up using it at your day job.

                                                                                                                  One of the reasons that TLA+ is so much easier to learn than so many other formal methods tools is that Leslie Lamport is, in my opinion, pretty much the best technical writer there is. So many formal methods books and papers are really tough to follow, even with lots of the background knowledge. I found Specifying Systems to be extremely easy to follow along with, and there’s even asides on math concepts when he feels that it’s useful.

                                                                                                                  Can’t recommend going down that path enough.

                                                                                                                1. 5

                                                                                                                  Elm, Godot and how to protect against and how to execute TLS man in the middle replay attacks (pointers to how to get started with this are warmly welcome!).

                                                                                                                  Also, more of: Rust, Blender, Renoise, BitWig, Octatrack, the game of Go (currently at ~4 kyu), ML and AVX2 assembly. Perhaps read a book or two about soft skills.

                                                                                                                  Maybe some more Zig and Agda, if time allows it.

                                                                                                                  1. 1

                                                                                                                    Wait, isn’t it the entire point of TLS that such attacks are impossible?

                                                                                                                    1. 3

                                                                                                                      MITM attacks are possible against anything that either doesn’t check the cert chain or which allows certs signed by malicious entities (the latter includes all web browsers, since the default certificate bundle includes things like the not-the-Turkish-Intelligence-service-honest root cert, among others). Replay attacks and downgrade attacks are possible against older versions of TLS, which is why there was a big push to get everyone onto 1.2 or later. Attacking an older TLS / SSL stack is a good exercise for learning why features are present (or, in some cases, absent) in the newer protocol versions.

                                                                                                                      1. 1

                                                                                                                        not-the-Turkish-Intelligence-service-honest root cert

                                                                                                                        Ouch, that sounds sexy, as in, a lot of things fucked. Can you write a short summary? Maybe backed by some links? Or just a link will do

                                                                                                                        1. 3

                                                                                                                          It looks as if that one (TURKTRUST) is gone now, after they were caught signing certificates for google.com for random people. The Turkish rep at one of the security conferences in the wake of this made such a big deal about this registrar not being in any way affiliated with their intelligence service that at the end no one believed him.

                                                                                                                          My system appears to have 158 trusted root certificates. Unless you’re doing DNSSEC and publishing CCA records, any one of them can sign a cert for any of your domains and my system will trust it. Want to bet that all of them are trustworthy?

                                                                                                                          1. 2

                                                                                                                            My system appears to have 158 trusted root certificates. Unless you’re doing DNSSEC and publishing CCA records, any one of them can sign a cert for any of your domains and my system will trust it. Want to bet that all of them are trustworthy?

                                                                                                                            Isn’t this what https://en.wikipedia.org/wiki/Certificate_Transparency addresses?

                                                                                                                            1. 2

                                                                                                                              Kind of. Certificate transparency lets you see if you’re seeing a different certificate to other folks or if the cert has changed. I think Chrome may be querying the CT logs when it sees a cert now (which has some privacy issues) but it’s not clear what constitutes a false failure and what a user should do if they see one. If the domain owner needs to update the CT logs (as seems to be the case in the new system - originally clients would report the certs that they saw to the CT service) then that means you now have a centralised single point of failure to accomplish exactly the same security guarantees that CCA records with DNSSEC give you.

                                                                                                                              CT checks also make it difficult to use something like Let’s Encrypt for non-routable domains with a split horizon DNS (which you can do with the DNS-based version of the ACME protocol) without also leaking the names to the public (they end up in the public CT log, forever). In exchange for this information leak, you get a weaker security guarantee than with CCA records. With a CCA record, if a malicious registrar provides a cert for your domain, it will not work. With CT, if a malicious registrar provides a cert for your domain then there’s an audit log that might let you know that some clients had their connections compromised.

                                                                                                                              1. 2

                                                                                                                                With CT, if a malicious registrar provides a cert for your domain then there’s an audit log that might let you know that some clients had their connections compromised.

                                                                                                                                The “might” isn’t really fair there. Significant efforts goes into this and the intent is not to flag an error to the user (which they might click through) but to be a deterrent and a way to identify bad actors. You have to be prepared to burn a CA if you choose to coerce it into issuing certs it shouldn’t, since it would have it’s trust revoked.

                                                                                                                                There is a “how it works” overview here: https://certificate.transparency.dev/howctworks/ and there aren’t single points of failure in the sense you suggest.

                                                                                                                                DNSSEC is not without its own problems, including adding several more failure modes. CT doesn’t seem to add any negatives.

                                                                                                                  1. 7

                                                                                                                    A computer inside the clock generator. I need to lie down.

                                                                                                                    1. 6

                                                                                                                      I’d rather have that than an uncalibrated clock. The method of using two clocks with different drift coefficients and using that to find the correct time is quite brilliant; the same method is used in the most accurate forms of radioactive dating. You could design and build a dedicated ASIC to do the same calculation, but then you’d have to get the damn thing fabricated, tested, etc and it would probably save you a few cents per package. Easier and faster to adapt an off-the-shelf part.

                                                                                                                      Edit: Upon re-reading, they never said there IS a CPU in the clock generator package, just that there’s room for one.

                                                                                                                    1. 2

                                                                                                                      I am perplexed by the very compact structure of the processor. What kind of external tools, if any, are used to design things like that?

                                                                                                                      1. 4

                                                                                                                        We use WorldEdit: https://dev.bukkit.org/projects/worldedit. On ORE, we also have a bunch of custom plug-ins to make certain things easier, such as this RedstoneTools plug-in: https://github.com/paulikauro/RedstoneTools

                                                                                                                        1. 1

                                                                                                                          MCEdit is a popular tool for this sort of thing, though I don’t know if it was used as such in this case.

                                                                                                                          1. 3

                                                                                                                            MCEdit also hasn’t been touched for years at this point, and doesn’t work with the newer versions of Minecraft :( There is Amulet (https://www.amuletmc.com/) that is attempting to be a more modern iteration of MCEdit but my experience with it has been mixed.

                                                                                                                        1. 3

                                                                                                                          What a coincidence, I was looking into learning Agda yesterday. Considering this short guide is far from complete and its last chapter is marked deprecated, are there any other good resources for learning Agda? As far as the ideas themselves of dependent types go, I’ve read “The Little Typer”, which gave me a good understanding of the fundamentals, but I’d like to read some more about things specific to Agda and the ways it is unique in the proof assistant landscape.

                                                                                                                          1. 3

                                                                                                                            I do wish there was a detailed comparison review / table / something of tools in the dependent types / proof assistant space… As someone trying to learn about this area, I currently find it quite hard to work how to choose between Coq, Idris, Agda, Lean, etc. At the moment, it feels like the people who know the area deeply enough to write such a thing are also heavily involved in one specific camp…

                                                                                                                            If anyone knows of such a resource, please do share it!

                                                                                                                            1. 5

                                                                                                                              I don’t know of such a resource, but as a very quick overview:

                                                                                                                              • Coq really is a theorem proved based on tactics, and supporting proof automation. Its syntax is ML-like. In Coq, one can write automated procedures to get rid of similar (or not-so-similar) cases for you. A great example is the Lia tactic, which automatically solves many proof goals with equalities and inequalities in them using some kind of algorithm. You never have to see the final proof object. It’s quite convenient. Another thing Coq has is extraction. It has built-in functionality for turning Coq code into, say, Haskell or OCaml. It’s not ideal, but you can verify a Coq program and then use it in some other project. The main downside of the language is, to me, its size. There are multiple sub-languages in Coq, with similar but different syntaxes. It’s a lot to learn. I also think the documentation could use some work.
                                                                                                                              • Where Coq lets you prove things via “tactics”, Agda lets you do so using standard proof objects and functions. I’ve seen it used for formalized mathematics and computer science (“Programming language foundations in Agda”, “Univalent foundations in Agda”), and also in multiple recent PL papers (a not-so-recent example is Hazel, a programming language whose semantics were formalized in Agda I believe). However, it’s also a much nicer language for actual dependently typed programming. It’s got a Haskell-like syntax and also some pretty nice support for custom notation and operators.
                                                                                                                              • Idris is also a Haskell-like language and it’s really geared towards dependently typed programming rather than proofs. It has some helper functions in its standard library for basic things (replacing one value with another equal value in a type, for example) but it’s far from convenient to write. In fact, Idris2 is (last I checked) not even sound. In it, Type : Type, which I believe can lead to a version of Russel’s paradox. Thus, you can technically prove anything. Idris’s new tagline is “language for type-driven development”. The approach that Edwin, the language’s creator, wants you to take is that of writing down types with a hole, and then gradually filling in the hole with code using the types to guide you.

                                                                                                                              I know you asked for a detailed review, but I thought maybe this would help.

                                                                                                                              1. 1

                                                                                                                                Thank you! Does anyone know enough about Lean to add a quick overview of it?

                                                                                                                            2. 3

                                                                                                                              Are there any other good resources for learning Agda

                                                                                                                              I’m going through PLFA, and there is an ongoing Discord study group here. For a concise 40-page introduction to Agda, see Dependently Typed Programming in Agda.

                                                                                                                              You might find some of the links I collect here on Agda interesting: https://www.srid.ca/agda

                                                                                                                              1. 2

                                                                                                                                Programming Language Foundations in Agda looks useful. Haven’t had the chance to dig into it yet though.

                                                                                                                                1. 1

                                                                                                                                  If you’re interested in using Agda as a vehicle to learning type theory, there’s also Introduction to Univalent Foundations of Mathematics with Agda, which isn’t exactly beginner material, though. Agda also itself supports cubical types, which kind of incepts the whole thing.

                                                                                                                                  In general, most of the material in Agda I’ve seen is oriented towards type theory and/or programming language research. It’d be interesting to see other mathematics as well.

                                                                                                                                  1. 1

                                                                                                                                    Thanks for the pointer! How feasible would it be in your opinion to understand this with only a few definitions’ worth of category theory knowledge?