jacobparker's comments

jacobparker | 1 year ago | on: Fidget

Coincidentally I was just reading this other wonderful post from the author https://www.mattkeeter.com/projects/constraints/

jacobparker | 1 year ago | on: Null-Restricted and Nullable Types

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!

jacobparker | 3 years ago | on: 1 TW of solar to be deployed annually by 2030

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.

jacobparker | 4 years ago | on: Show HN: Dependently typed language for proofs that you can implement in one day

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...

jacobparker | 4 years ago | on: Show HN: Dependently typed language for proofs that you can implement in one day

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.

jacobparker | 4 years ago | on: Bringing supply chain security features to the Go community

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.

jacobparker | 5 years ago | on: We found and fixed a rare race condition in our session handling

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.

jacobparker | 5 years ago | on: RFC 8959: The “secret-token” URI Scheme

Ah, thank you.

jacobparker | 5 years ago | on: RFC 8959: The “secret-token” URI Scheme