  Text editors represent one of the fundamental tools that writers use -
software developers, book authors, mathematicians. A text editor must work as
intended in that it should allow the users to do their job. We start by
introducing a small subset of a text editor - line editor. Next, we will give a
concrete definition (specification) of what a complete text editor means.
Afterward, we will provide an implementation of a line editor in Coq, and then
we will prove that it is a complete text editor.
