1. jacobparker Jan 8, 2025 parent

   Coincidentally I was just reading this other wonderful post from the author https://www.mattkeeter.com/projects/constraints/
2. jacobparker Aug 2, 2024 parent

   The one nullable gotcha with doing this is that the .NET standard library doesn't have nullable annotations in older frameworks.

   One approach to adding nullable annotations to a large code-base is to go "bottom-up" on DLL at a time. The annotations are somewhat viral; if you were to go top-down then as you get to more of the "shared" DLLs and add annotations you'll find yourself having to go back and revisit the DLLs you already migrated. In this light, the .NET standard library situation is problematic.

   Imagine implementing IEnumerable<T> by wrapping another IEnumerable<T>; in .NET framework there are no nullable annotations, so you can get into a situation where you don't add a nullable annotation where you will eventually need one upgrading to newer .NET. This can bubble up throughout your code base, making that eventual .NET upgrade more challenging.

   I'm not saying its not worth it to do this in .NET framework, but you can very easily add extra work to the inevitable(?) update to .NET 8+. When you get there you could of course temporarily regress and turn nullable stuff back to warnings until you work through that surprise backlog, but nullable is really nice so you might be strongly inclined to not do that... not a huge problem, just something to be aware of!

3. 1 point Sep 1, 2023

   There’s a Source of Clean Energy Beneath Our Feet. and a Race to Tap It

   1 comment jacobparker nytimes.com
4. jacobparker May 19, 2022 parent

   Consider that 40% of American corn crop (created, as you say, by redirecting the suns energy) is turned into Ethanol, to be burned for energy.

   Solar panels are "roughly 200 times more energy per acre than corn" according to https://pv-magazine-usa.com/2022/03/10/solarfood-in-ethanol-...

   There are ecological concerns but the alternatives have them too.

5. jacobparker Oct 3, 2021 parent

   I highly recommend SF. The trick is you must use the books via coqIDE or something equivalent; viewing the rendered HTML is almost pointless at best, but probably counter-productive.

   Binary search would be a good exercise. I think SF volume 1 would be more than enough, with the exception of deciding how to model arrays (you'd probably want to look up Coq's persistent arrays/PArray system for this.) SF volume 3 does binary search _trees_ which is similar but avoids the array problem (as is customary in functional languages.)

   However, Coq (by default) also uses infinite precision numbers. This works very well for proofs but isn't necessarily realistic. This is where some extra fun comes in: fixed precision arithmetic is a very common source of bugs for binary search: https://ai.googleblog.com/2006/06/extra-extra-read-all-about...

6. jacobparker Oct 2, 2021 parent

   Some examples from a Software Foundations (a series of books about Coq, available online):

   I just wrote something I called insertion sort. I want to know that this is a valid implementation of sorting. What does it mean to be a sorting algorithm? It means that the output is sorted, and it's a permutation (shuffling) of the input. This is an exercise here: https://softwarefoundations.cis.upenn.edu/vfa-current/Sort.h...

   Say I've written a Red-Black tree. I want to know that it behaves like a map, or that it keeps the tree appropriately balanced (which is related to performance): https://softwarefoundations.cis.upenn.edu/vfa-current/Redbla...

   One more: say you have specified a programming language, which includes describing the structure of programs (the grammar essentially) and "small step" semantics (e.g `if true then x else y` can take a step to `x`). It would be interesting to show that any well-typed halting program can be evaluated in multiple steps to exactly one value (i.e. the language is deterministic and "doesn't get stuck" (or, in a sense, have undefined behaviour)). That's the subject of volume 2 https://softwarefoundations.cis.upenn.edu/plf-current/toc.ht... Beyond this, you may have done a similar thing for a lower level language (machine assembly, wasm, ...) and have a compiler from your language to the low level language. You may want to prove that the compiler "preserves" something, e.g. the compiled output evaluates to the same result ultimately.

   RE: termination, in something like Coq that is a bit special because every function terminates by construction. That might sound limiting but it's not really/there are ways around it. It would, however, be impossible to write something like the Collatz function in Coq and extract it in the obvious sense.

   EDIT: and there are other ways these tools can (theoretically) be used to work with programs, but that's a long story. There have been real-world programs built like this, but it is very uncommon at this time. It is an area of active research.

7. jacobparker Jul 23, 2021 parent

   For NuGet, consider using centralized package references: https://github.com/NuGet/Home/wiki/Centrally-managing-NuGet-...

   You get one file defining the set of all packages used in your repo (or some subset of your repo, etc.) and Dependabot will update this file directly. Individual projects can choose to use a package but won't specify the version.

   It requires that your projects are all in sync with package versions but (1) that sounds like what you want (2) it's usually the best thing.

8. jacobparker Mar 19, 2021 parent

   At D2L we have a large C# code base which gets deployed in a few different subsets, but is largely a monolithic fleet of web servers.

   To prevent these kind of problems we have a few approaches, but the main way is to prevent shared mutable state. To do this we have a custom C# code analyzer (source here: https://github.com/Brightspace/D2L.CodeStyle/tree/master/src... , but it's not documented for external consumption at this point... ImmutableDefinitionChecker is the main place to look.) It goes like this:

     [Immutable]
     public class Foo : Bar {
       // object is a scary field type, but "new object()"
       // is always an immutable value.
       private readonly object m_lock = new object();
     
       // we'll check that ISomething is [Immutable] here
       private readonly ISomething m_something;
     
       // Fine because this lambdas in initializers can't
       // close over mutable state that we wouldn't
       // otherwise catch.
       private readonly Action m_abc = () => {};
     
       // see the constructor
       private readonly Func<int, int> m_xyz;
     
       // danger: not readonly
       private int m_zzz;
   
       // danger: arrays are always mutable
       private readonly int[] m_array1 new[]{ 1, 2, 3 };
   
       // ok
       private readonly ImmutableArray<int> m_array2
         = ImmutableArray.Create( 1, 2, 3 );
     
       public Foo( ISomething something ) {
         m_something = something;
     
         // ok: static lambdas can't close over mutable state
         m_xyz = static _ => 3;
     
         // danger: lambdas can in general close over mutable
         // state.
         int i = 0;
         m_xyz = x => { i += x; return i; };
       }
     }
   

   Here we see that a type has the [Immutable] attribute on this class, so we will check that all the members are readonly and also contain immutable values (via looking at all assignments, which is easy for readonly fields/properties). Additionally, we will check that instances of Bar (our base class) are known to be immutable.

   Any class that were to extend Foo (as a base class) will be required to be [Immutable] as well. There's a decent number of aspects to this analysis (e.g. a generic type can be "conditionally immutable" -- ImmutableArray<int> is, but ImmutableArray<object> is not), check the source if you're interested.

   We require all static (global) variables be immutable, and any "singleton" type (of which we have tens of thousands if I remember correctly) also must be.

   Another important thing we do to is to cut off any deferred boot-up code from accessing customer data (via a thread-local variable that is checked before access through the data layer). This prevents accidentally caching something for a particular customer inside, say, a persistent Lazy<T> (or the constructor for a singleton, etc.)

   We've adapted our code base to be very strict about this over the last few years and it discovered many obscure thread-safety bugs and doubtlessly prevented many from happening since.

9. jacobparker Feb 3, 2021 parent

   Ah, thank you.
10. jacobparker Jan 31, 2021 parent

    You might be interested in:

    git config --global core.excludesfile ~/.gitignore

    You can have a system-wide (but local only) .gitignore. It doesn't help other people who clone your repo, but it can be useful in some situations.

11. jacobparker Jul 27, 2020 parent

    For the past few years the performance work (e.g. commit graph) has made a huge difference for large/fast moving repos. They're big enough to be productivity enhancements for some people: when we merged our Android-like multi-repo setup into a proper mono-repo we required updating git because things like git status/git commit/git log could take minutes without the recent perf fixes.

    It pays to follow the release notes because some of these features are opt-in (e.g. commit graph is still optional).

    The sparse checkout stuff is great but still too low-level for us to use, but it's laying the groundwork for something good.

12. jacobparker Jul 25, 2020 parent

    > where the builds run on your own hardware

    This is possible with GitHub Actions, too: https://docs.github.com/en/actions/hosting-your-own-runners/... (the place I work at uses it.)

13. jacobparker Jun 17, 2020 parent

    Thanks for the reply. What do you mean by a CI/CD system?

    I'm not sure what you think was "bolted on" to actions, could you be specific? Features have been added (during the beta and since) but I can't think of anything that could really be described as "bolted on". "bolted on" to me implies some kind of disharmony with other features, weird quirks etc.

    > I seriously didn't understand what problems github actions were intended to solve

    You can run arbitrary code in response to any GitHub repository event, and also cron jobs and external triggers (a GitHub app can POST to a specific API to trigger those style of workflows).

    The code runs with access to GitHub APIs for your repo (it can clone it, leave comments, create new PRs, whatever), and in any event that is associated with a PR a check status gets added to the PR.

    This is a pretty general-purpose tool and I think it's easy to imagine the kind of problems people would use it to solve...

    > my suspicion is [...]

    Honestly it sounds like you're not really familiar with it and have some strongly negative opinions. I'd recommend either giving it another look and putting aside your feelings or working on a more substantive critique...

14. jacobparker Jun 17, 2020 parent

    You can do just "on: push" if you don't need filters like branches/paths/etc. :)
15. jacobparker Jun 17, 2020 parent

    It's really hard to understand what you're trying to say here. I use actions a lot. There is no distinction between actions and CI/CD here. The context of this blog post is a set of features that were added to actions (during the beta!) to better support CI/CD workflows. There is no CI/CD "shortcut", like you say, bolted on to actions.

    The alpha was rougher (and completely different) but that's why it was called an alpha!

16. jacobparker May 30, 2020 parent

    OP said safely; what you're describing isn't safe in, say, C++ in the same sense that it is in Rust.
17. jacobparker Apr 28, 2020 parent

    Any other argument for a different base aside, in base 12 you have the analogous “problem” that 0.BBB... = 1. None of the usual bases, equipped with this “...” power, avoid the “problem” (non-unique representation).
18. jacobparker Apr 20, 2020 parent

    > When you get down to it, between cache coherency across CPUs and memory, disk flush delays and disk caches, every database is eventually consistent.

    This is a false. None of the things you listed preclude consistency.

    > And if you want to operate over a distributed network, which means you WILL have network partitions, then you are subject to CAP and will need eventual consistency mechanisms.

    That's not how CAP works. Plenty of distributed CP databases exist.

19. jacobparker Apr 16, 2020 parent

    Right, but the reasons why are different from the halting problem. As stated in the OP, "the key assumption in this argument is continuity". I'm not sure what you mean by the outputs being "expected to be considered a continuous function". In both the halting problem and this case the outputs are discrete (e.g. binary: halts/does not halt, left/right, etc.)

    There are other impossibilty results, e.g. the FLP theorem. Despite having computing-based interpretations they're not all related to the halting problem. :)

    That being said, maybe it's possible to generalize the halting problem to a continuity in some reasonable way and get something like Buridan's principle. It's not obvious to me how that would be done but I'd be interested to see!

20. jacobparker Apr 16, 2020 parent

    It's an interesting thought but I'm not aware of any way to plausibly connect the two, mathematically.
21. jacobparker Apr 3, 2020 parent

    Mostly, if you opt in: https://caniuse.com/#feat=same-site-cookie-attribute . SameSite=Lax will still send cookies for some types of GET requests, depending on the complexity of your site and UX there are ways to be more protected (with SameSite=Strict, cookie pairs etc.)

    Once all browsers behave like Chrome is trying to (SameSite=Lax by default) we will have dramatically less CSRF on the web. Other browsers are likely to adopt this change eventually if Chrome sticks with it. You will at least need to consider users with out-of-date browsers for a while yet (and implement XSRF tokens and/or explicitly opt-in to Lax/whatever).

    The old behaviour will still (and always?) be around with SameSite=None. It has uses, but misuses could create CSRF vulnerabilities. There will still be CSRF problems on the web but it will get a lot rarer and, mercifully, not the default.

22. jacobparker Feb 28, 2020 parent

    Google is already a CA.

    https://pki.google.com

23. jacobparker Feb 12, 2020 parent

    Wildcards have use cases. An example:

    You have a .example-usercontent.com wildcard certificate for domains like user-1234.example-usercontent.com and you have millions of users. A wildcard certificate is appropriate because:

    * LetsEncrypt rate limits are a thing

    * The domains exist to leverage origin sandboxing in browsers, but are served by the same infrastructure. It's not more secure (but it is more complicated) to have more certificates here.

    Generally, the assumption that two subdomains are served by independent infrastructure is often wrong. Think of things like blogger.com/blogspot.com. So the concern about compromising keys doesn't really apply.

24. jacobparker Jan 5, 2020 parent

    Ah, good point. So it depends on your site. Some sites need to do things like serve embeddable content or be an OAuth identity provider, etc., and SameSite=None is required in those cases. Sorry for not being more clear about that.
25. jacobparker Jan 5, 2020 parent

    > So user-agent sniffing will probably be necessary for years.

    Only if you set None (either to opt-out or to do a None/Strict pair). Setting Lax doesn't require sniffing.

    But yeah, that seems like a safe bet.

26. jacobparker Jan 5, 2020 parent

    Interesting theory. I don't think it's true, though. The original spec mandated case-insensitive comparisons and it looks like WebKit has always been doing that to me.
27. jacobparker Jan 4, 2020 parent

    Yep, that's the issue. I think I see the confusion now (I stand by my original comment).

    SameSite=Lax was never an invalid value, so it was never mishandled by browsers (very old browsers gracefully degrade to treating it like None, which is as good as possible). In the original spec there was Lax, Strict, and unspecified (i.e. the Set-Cookie header didn't have a SameSite attribute, the default behaviour) but, critically, no None.

    Browsers developed around that time that treated unexpected values as equivalent to unspecified/what we now call None (e.g. Firefox) turned out to have picked a more forwards-compatible approach. Browsers like Safari and Chrome took stricter action for unexpected values (the idea here is a vague "secure by default" feeling) but it's awkward now that the default is changing from what is (now) called None, to Lax.

    In that issue, consider the title "Cookies with SameSite=None or SameSite=invalid treated as Strict" redundant: None was an invalid value according to Safari at that time, which wasn't wrong.

    SameSite=Lax is 100% safe to set (assuming your site is ready for that). You only need to browser sniff if you're considering setting SameSite=None.

28. jacobparker Jan 4, 2020 parent

    You mean block all SameSite=None cookies? They have legitimate uses too.

    Consider that SameSite=Strict even breaks cross-origin links (<a> tags): if a 3rd party site links to you and a user clicks that link, the GET will be sent without cookies.

    To get value out of Strict for typical sites the new pattern is to have two cookies: one is SameSite=None and allows you to do GET/HEAD/etc. requests ("read-only operations", assuming you are following those parts of the spec) and one that is SameSite=Strict and allows you to do POST/etc. ("write operations").

    If https://evil.com adds a link to your site (an <a> tag) you can allow deep linking by only checking for the None cookie. The strict cookie won't be sent for <a> tags. But POSTs/form-submissions, and any page/resource you don't want to allow deep-linking for, you would check for both the cookies.

    I've seen this pattern referred to as "reader and writer cookie pairs".

    ---

    This really is specifically aimed at killing CSRF attacks. It's not about tracking either way (it's orthogonal to that).

29. jacobparker Jan 4, 2020 parent

    Hey, there are some important mistakes in this warning:

    1. The value that is invalid for older browsers (including older versions of Chrome!) is None, not Lax. It is always (as far as anyone knows safe to explicitly set SameSite=Lax in all browsers, assuming your site is ready for that.

    2. The latest Safari (v13) has changed their behaviour to match the latest spec.

    See this article for details on detecting/dealing with it: https://www.chromium.org/updates/same-site/incompatible-clie...

    TL;DR: old (but not too old) Chrome responds by rejecting the cookie entirely (which Google says was an valid interpretation of the spec, at the time of those versions) and old (but not too old) Safari responds by interpreting the None value as Strict (I think there is some debate on whether the spec allowed this back then, but at this point it doesn't matter/I don't care).

This user hasn’t submitted anything.