jacobparker

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.

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

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.

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.

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; };
    }
  }

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.

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