The problem is introduced and proven (manually) here: https://leimao.github.io/blog/Proof-Container-With-Most-Water-Problem/
We’ll do the proof in Dafny.
Continue reading “Dafny proof to the Container With Most Water Problem”
Author: Boro Sitnikovski
GEB: An EGB overview (Part I)
I’d started some time ago, and just recently finished reading the first part of Gödel, Escher, Bach: An Eternal Golden Braid. Here, I will present my quick overview of each chapter.
Infinite power towers
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”
bor0's reflective blog 