Literate formal math

In my spare time, I like to develop formal mathematics using the proof assistant and programming language Agda. Here is a screenshot of what my latest code looks like:

This is an html-rendering of the latest version of my code hosted here:

https://felix-cherubini.de/sag/Cubical.AlgebraicGeometry.Spec.html

My post is not about the mathematical content – that can safely be ignored for the matter of this post. What I want to show you is, what the code (and the html generated from it) looks like. If you want to look at the source for this file on github, you have to use ‘raw’-view, since github uses the ending to decide, that it should be rendered like a markdown file:

https://raw.githubusercontent.com/felixwellen/cubical/basic-algebraic-geometry/Cubical/AlgebraicGeometry/Spec.lagda.md

One thing I am constantly dissatisfied with when writing mathematics as formal code, is, that the result is usually far less readable than mathematical articles or textbooks. Most things I wrote recently in Agda, just look like functional source code and should not be too inviting for everyone in my target audience. Of course, when thinking about my math code, I always ask myself, if something working there, carries over to practical programming. I guess in this case I am just rediscovering the fun of something quite old and well known in practical programming.

Until about a month ago, the best remedies for my not so well readable math code, was to extensively use Agda’s mixfix syntax, math symbols via unicode and large comments, sometimes even with diagrams in ascii-art. While my mixfix use turned out to be a bit too much, the other two things work quite ok. However, above I showed you the results of somethin I tried quite late: literate programming!

I learnt how to use Agda’s limited literate programming capabilites together with some pandoc-postprocessing here:

https://jesper.sikanda.be/posts/literate-agda.html

I knew about the literate programming features, but I underestimated the difference it makes. What I use so far, amounts to not much more than having comments, that are rendered to html in some way. The real difference is, that I start with the text explaining what the code is about.

I am pretty sure though, that I would probably not have started to use it so enthusiasticly, if I hadn’t been writing math. This is because literate math coding let’s you mix prose and math code in very much the same way as it is usually done when writing math the traditional way. So one could say that I learnt already how to write literate code in my mathematical education, which allows me now to do it now without too much thinking and discipline.

I do not think, that it is a good idea to write all code like that. In the example above, my goal is to write some interesting math story which leaves out a lot of details which are hidden away. In a practical project, it might help to write, say, the main method in this style to give a top level explanation on how things are organized.

Let me have a pass around my main point again: It helps a lot to have a text file, which also contains code instead of a code file, which also contains text (i.e. comments). It made me think that I am editing a text file, when editing the literate code. Which is great, because it helps against my main problem with comments: I forget to change them, because they are not a part of the code.

return first

Let me introduce the “return first” method? Fear not, this is not a treatise on guard-clauses. What it is, is both a code design approach and a refactoring method. It starts with a simple question to ask yourself whenever you want to call a function:

Can I return first?

That’s supposed to be catchy, but it is probably not terribly enlightening. Let me demonstrate with an example. I’ll be using C++, but I dare say that this method can be used in all imperative languages.

void process_all(
  std::vector<input_info_t>& input_list,
  context_t const& context,
  target_t const& target)
{
  for (auto& each : input_list)
  {
    if (some_filter_applies(each, context))
    {
      hand_off_to(each, target);
      continue;
    }
    
    process_one(each, context);
    hand_off_to(each, target);
  }
}

For the sake of this example, the three functions some_filter_applies, process_one and hand_off_to are immutable. Let us try to improve process_all by extracting a function:

void maybe_process_and_hand_off(
  input_info_t& input,
  context_t const& context,
  target_t const& target)
{
  if (some_filter_applies(input, context))
  {
    hand_off_to(input, target);
    return;
  }
  
  process_one(input, context);
  hand_off_to(input, target);
}

void process_all(
  std::vector<input_info_t>& input_list,
  context_t const& context,
  target_t const& target)
{
  for (auto& each : input_list)
  {
    maybe_process_and_hand_off(each, context, target);
  }
}

So what do we have now:

  1. 26 instead of 17 lines. 22 instead of 13 if we do not count lines with just braces, a 70% increase.
  2. A pretty clumsy name for the function called in the loop. Can you do better?
  3. We have to pass the target all the way to hand_off_to without really using it directly in maybe_process_and_hand_off.
  4. The complexity is more or less the same.

So that was not great. So let us try to use return first and focus on hand_off_to. What if instead of calling hand_off_to, we just return first, and then do it? In this case, it’s pretty easy, since hand_off_to is a tail-call in each case:

void maybe_process(
  input_info_t& input,
  context_t const& context)
{
  if (some_filter_applies(input, context))
  {
    return;
  }
  
  process_one(input, context);
}

void process_all(
  std::vector<input_info_t>& input_list,
  context_t const& context,
  target_t const& target)
{
  for (auto& each : input_list)
  {
    maybe_process(each, context);
    hand_off_to(each, target);
  }
}

Now we no longer have to pass target through a function that does not need it, which makes both the call site and the function declaration simpler. Now a few more other refactorings are available. Let’s assume some_filter_applies is pure and process_one only changes its input parameter, as the signatures suggest. We can use loop fission, and inline the function again:

void process_all(
  std::vector<input_info_t>& input_list,
  context_t const& context,
  target_t const& target)
{
  for (auto& each : input_list)
  {
    if (some_filter_applies(each, context))
    {
      continue;
    }
  
    process_one(each, context);
  }
  for (auto const& each : input_list)
  {
    hand_off_to(each, target);
  }
}

“return first” actually works for all control structures, not just functions. So in this case we returned from the first loop before starting to call hand_off_to multiple times. Often times, the code will not be as easy to refactor, because there is actually some data flowing between the function we’re in and the one we’re calling. The simple solution then is to pack all the parameters into a struct and return that, aka using data as the interface instead.

void hand_off_individually(
  std::vector<input_info_t>& input_list)
{
  for (auto& each : input_list)
  {
    auto target = compute_target(each);
    if (!target.valid())
      continue;

    hand_off_to(each, target);
  }
}

That be turned into this:

void hand_off_individually(
  std::vector<input_info_t> const& input_list)
{
  struct targeted
  {
    input_info_t info;
    target_t target;
  };
  std::vector<targeted> valid;
  for (auto const& each : input_list)
  {
    auto target = compute_target(each);
    if (!target.valid())
      continue;
    valid.push_back({each, target});
  }

  for (auto const& each : valid)
  {
    hand_off_to(each.info, each.target);
  }
}

This is definitely longer, and probably not worth the hassle for this contrived example – this is more to show how to do it, not that is is effective.

Evaluation

In real programs, this applying “return first” is often worthwhile. It makes the code flow “wider instead of deeper”, which is often easier to follow, especially if you try to debug or measure/profile your code. It is also a gold-recipe to enable batching, which is curcial whenever you’re dealing with latency, e.g. when using RAM or building web requests. Have you tried this technique before? Do you, maybe, know it by another name? Do tell!

Key ingredients for the home office

Since March 2020, we transformed from an “on-site” company to a remote company, not particularly because we wanted to, but because the corona pandemic forced us to. Our office is not suitable to ensure transmission safety, so I decided that work from home is the lesser problem. When I say “transform” and “decided”, please bear in mind that these are retrospect notions. The decision was made at Monday, March 16th 2020 and the transformation happened in the next two days.

But there is a real difference between being operable and fully equipped for the situation. We were operable in the remote situation within 48 hours. But we still work on improving our equipment to match the situation that seems to linger a lot longer than initially anticipated. This blog post tries to summarize what we’ve learned since March 2020 in regards to equipping home office workplaces past the makeshift phase.

The fundamentals

The most fundamental ingredients of any office workplace are the table and the chair. If any of those lack in necessary ergonomic features, your comfort will never be the same as in the office (provided that your equipment there is adequate). And this constant discomfort will permeat everything you do.

The chair was easier to detect because it shows up in the video calls, it is part of the “zoom room”. Still, it took some time to order new chairs or transport existing office chairs to the home offices. If you experience back pain or mechanically induced headaches, review your chair thoroughly.

The table was more tricky, because it is typically invisible during video calls. My approach was to retrieve a photo of every home office space and talk about the possible improvements. During these talks, we came up with two solution categories that I want to present.

The notebook workplace

We all had work notebooks as secondary computers before the pandemic. So it was not a problem to start with working from home on that notebook, we’ve done it before. But if all you do is to work directly at a notebook, you might have the best chair and table, your body posture will be suboptimal. We equipped the notebook-based workplaces with the following extras:

  • An external keyboard
  • An external computer mouse
  • One (or better: two) additional monitors
  • A matching docking station, at least to connect to the monitors
  • A notebook riser stand

The last item, the notebook riser stand, was the game changer when it came to multi-monitoring (two or three monitors). It elevates your notebook to the same height as the other displays and might even change its angle. This transforms your notebook from being the CPU unit with cumbersome monitor to a secondary monitor with a CPU. The riser stand doesn’t cost much (if you don’t go overboard with its design) and provides you with more table space and improved displays.

The existing computer workplace

Because we are software developers, we mostly have a very decent computer already fully equipped at home. The only problem: The computer is for private tasks and should stay that way. We want to separate our work environment from our leisure environment as much as possible. But several developers wanted to use their usual “battlestation” for home office work, too.

In this case, we bought a lavish SSD as an additional boot drive for the home PC. This separates the work operating system from the leisure drive as much as the notebook approach. And the existing hardware can be used for both timeslots, much to the comfort of the developer.

The video conference equipment

But regardless of your approach (notebook or existing computer), there are still some things missing that improve the quality of work of yourself and your colleagues tremendously:

  • A good headset, preferably with top-notch comfort and active noise cancelling (ANC)
  • An at least decent webcam

Most notebooks provide a mediocre webcam and some low quality microphone. Do yourself (and your communication partners) a favor and invest in a good microphone. Oftentimes, it is coupled with good headphones. The difference between a good audio setup and an echo-prone makeshift solution is the deciding factor when essentially all communication with your colleagues go through this channel.

The webcam is not as essential as the audio equipment, because it “only” affects your communication partners, but it adds a nice touch to your other equipment. You don’t have to go overboard on it, a model for one hundred euros is already an improvement.

The bottleneck

One thing that can really invalidate most of the other improvements is a small internet connection. This is probably to hardest thing to fix in a timely manner, but give it some thoughts. If your internet connection is too slow for your daily work and communication pattern, it will be a constant annoyance. Just because it takes some time to improve doesn’t mean you shouldn’t try.

We will probably remain in this situation long enough to still reap the profit of our effort. And even if not (at least we can hope), nobody ever complained about an internet connection that is a bit oversized.

TL;DR

If you didn’t read the article, here are the major take-away points neatly summarized:

  • Ergonomic chair and table
  • Notebook with external keyboard, mouse and monitor
  • Notebook riser stand
  • SSD for dual boot systems
  • Good headset
  • External webcam
  • “Broadband” internet

If you miss an item from this list for your home office, give it a thought. And if you plan to only think about one item, think about your chair first.

What are your experiences with working from home? What accessory makes your work life better? Give us a hint by writing a comment below. Thank you!

Windows 10 quality of life features

Starting with Windows 10 Microsoft switched from big-bang releases of its operating system to so called rolling releases: They release new features and improvements in regular intervals – once or twice a year – without changing the product name.

The great thing is that users get the improvements made by Microsofts engineers much sooner than in the past where you had to wait several years for a big “service pack” to arrive or even a new major release of Windows like 2000, XP, Vista, 7, 8, 8.1 and finally 10 (I am leaving out the dark times on purpose 😉).

The bad thing is that it is harder to see what version or release you are running. Of course there is a (less visible) name for every Windows release. This version or codename sometimes gets mentioned on support pages or in blog posts because functionality of Window 10 can change significantly between these rolling feature updates. And sometimes you may run some app or tool that tells you need Windows 10 2004 or higher.

What version of Window 10 am I running?

I know of two simple ways to find out what version of Windows 10 you are running currently:

  1. Running the tool winver
  2. Opening the Settings -> System -> Info page

Why does it matter?

Another downside is that users often are not aware of new stuff added to their operating system. And Microsoft does an awful job promoting the changes and improvements!

Of course there are announcements about the big things after upgrading your operating system to the next feature level. And Microsoft uses these for marketing its own apps and services. They slap you their new Edge-browser in the face on every occasion and try to trick you in creating a Microsoft account. It is absolutely not obvious how to use Windows without a Microsoft account like the decades before. Skip the process here, continue without and risk your live…

On the other hand they really improve their software and slowly but steadily round the rough edges of their system. The UIs for environment variables are finally quite usable.

Now back to the main theme of the post: There are some hidden gems built into Windows 10 that I learned of only lately and I think are vastly underadvertised – unlike Microsoft’s marketing of their big products.

Built-in screen recorder

Ok, many gamers may know it because it Windows briefly displays the shortcut Win+G when starting a game. It is not only usable for games but you can record any window, capture application sounds and record your voice. You can easily record your own screencasts and video tutorials using this built-in solution.

Built-in clipboard manager

How often did you wish to be able copy multiple items and choose one of the last few copied elements when pasting? While such clipboard managers have been around for a long time and sometimes provide tons of useful features Windows 10 has a simple one built-in. Just press Win+V instead of Ctrl+V to paste your clipboard entry and you will get a list of the copied items to choose from.

Built-in screenshot/snipping tool

Many people may know the old way of making screenshots using the oddly labeled PrtScr-key (sometimes also PrntScrn or simply Print), opening a painting application like MS paint and pasting the image using Ctrl+V. Well, Microsoft improved this workflow a lot by including a snipping tool that you can activate using Win+Shift+S. This tool lets you select either a rectangular or free-form region, a window or an entire screen to capture. After doing that you get a notification allowing you to make modifications to the capture and save it to disk.

On-screen emoji-keyboard

Just a little helper in these modern social media times is the on-screen emoji-keyboard. Using Win+. you can activate it, browse tons of common emojis and enter them into you messages and texts 🐱‍🏍🤘.

Windows Terminal

Ok, this last but not least one is not (yet) built-in and mostly interesting for developers and power users. Nevertheless, I think it is noteworthy that Microsoft finally built a capable terminal application with modern features like multiple tabs, full unicode and font support, customizable background with blur and the ability to host different shells like the old and trusted command prompt CMD, the newer PowerShell and WSL. You can find it in the Microsoft store for free.

Conclusion

While releases of Windows 10 are more subtle than past new Windows releases many things change both under the hood and user visible. Every once in a while something you missed for years or installed third-party tools for may be added without you knowing. That’s another reason why talking to colleagues and friends and practices like pair-programming and brown-bag meetings are so valuable for sharing knowledge and experience.

I hope there is something for you in my findings of hidden windows gems. If you have some Windows 10 features you discovered and really like, feel free to leave them in the comments. I will gladly try them out!