A few days ago I read an interesting problem on Hacker news:
Find 
Idea: news diversity
As with most of my mornings, they start with a coffee and reading the news on time.mk – news portals' aggregator.
At the time of writing this post, there are about 115 sources on the sources list on time.mk. As readers, we are mostly interested in unique content. Out of those 115 sources, a lot of them will generate noise. It may look something like this:
Even if you don’t understand Cyrillic, you can tell it’s definitely the same text.
So, how do we find the most unique sources and only stick to them, instead of wasting our time on copy-paste news portals that do not produce original content?
Formalizing expressiveness of line editors
According to Wikipedia, a line editor is a text editor in which each editing command applies to one or more complete lines of text designated by the user.
We will implement our own line editor in Coq, and then we will prove that it is a complete text editor.
Continue reading “Formalizing expressiveness of line editors”
Proving Groups with Idris
Exactly a year ago, in one of my previous posts, we proved Monoid laws with Idris. We’ll do the same with Groups.
A8c team meetup Athens, 2019
During the first week of October, we had our team meetup in Athens, Greece.
We had a lot of projects going on, and one of them (which I was involved in) was working on the architecture of WooCommerce Services. It has wp-calypso as a dependency, and we wanted to move out of that and just rely on @wordpress/components. We have a PoC PR and wrote an internal P2 post about it.
Fun stuff, right? Now for the actual fun stuff. We did a lot of escape rooms. And I mean a lot.
bor0's reflective blog 