# Book review: Developer Hegemony

At the end of 2018, I searched for new software development books to read and came across a list that spiked my interest. My impulse was to buy and read all five books. I’ve bought them all, but only read four of them yet. You can read another book review from this list in a previous blog post.

The book I was most sceptical about came with a black cover and the menacing title “Developer Hegemony” by Erik Dietrich. It’s not a book about software development, it is a book about the industry of software development and why it is fundamentally different than “traditional” industries. And it is a book that promises an outlook on “the future of labor”, at least for us developers. Spoiler: It’s not about taking over the world, as the cover image suggests. It’s about finding your way in an industry that is in very high demand and mostly consists of players that play by the rules of an entirely different game: industrial manufacturing.

Let’s have a short overview about the content: My impression of the book was that it consists of three parts, even if there are five distinct parts in the table of contents:

• The first part takes a good hard look on the current situation and identifies the losers and “winners” of the game. It introduces a taxonomy of industry employees that all give up on something in exchange for some personal gain. What that something is depends on the worker type. This is like the setting up on a chess board. You get to know the pieces and their characteristics and realize that they are mostly pawn cannon fodder.
• The second part puts the taxonomy in action and describes the carnage unfolding on the chess board. The grim message is that the only winning move is to own the board itself and make up the rules, but never participate in the game. And if you find yourself on the board, keep moving sideways like the bishop and change your color often. Don’t associate with any team and don’t engage in any stalemate situations. The author describes the “delivery game” very illustrative: If you are responsible of delivering something, you might succeed, but you can also fail. If you are only responsible of counseling a delivery, you can attach yourself to success and detach from failure more easily. Be the bishop and evade delivery responsibility by an elegant sidestep. This part is especially gruesome because it describes in detail how technical expertise in software development is a recipe to remain at the center of the delivery game. It makes every passionate developer’s heart ache.
• The third and last part shows an alternative to the “own the board or be a pawn” dichotomy. Emotionally, it rescues the developer enthusiast. The message is soothing: You can continue to develop software, but you have to step up and own the results of your development, too. This means effectively being self-employed and acting like a business entity. Yes, I’ve said it wrong: I meant being self-employed and being a business entity. You can probably count on being in high demand for years to come, so the step from “developer” to “entrepreneur” is not as big as you probably are afraid of. And you don’t need to be strictly alone: Find partners and associate with them. But don’t stop being your own business entity. Don’t shed your self-confidence: You are the world’s most sought-after expert.

This book left me speechless. I’ve founded my company nearly twenty years ago without Erik Dietrich’s experience, just based on my beliefs that I couldn’t even articulate. And now he spelled them out for me in detail. Don’t get me wrong: My company is different from Erik Dietrich’s ideal of an “efficiencer company” in many details, but in the root of the matter, this book describes my strategic business alignment and my reasons for it perfectly.

But even besides my own affection to the topic, the book provides a crystal clear view on the software industry and a lot food for thought. Even if you don’t plan to leave your corporate job anytime soon, you should at least be clear about the mechanics of the game you participate in. The rules might differ from company to company, but the mechanics stay the same.

Do yourself a favor and read this book. You don’t have to change anything about your job situation, but you are invited to think about your stance and position in this industry. For my last sentence in this blog entry, let me spoil you one main difference of our industry in comparison to others: If all you need to develop first-class software is a decent notebook and some coffee, why are you still depending on your employer to provide both for you in exchange of all the surplus of your work? That’s the world’s most expensive coffee.

# A new star in software verification?

F* (pronounced F star) is a functional programming language with a dependent type system that supports verification. What follows is a story about my experiences with F* and a concluding opinion why languages like F* could be useful for the working software developer.

There is a big project using F* and related tools for the ambitious goal to build a verified implementation of TLS.
So far, judging from the website, there is a verified efficient implementation of the relevant cryptographic primitives but their implementation of the protocol is not yet verified. That is certainly already a great achievement and got me interested F*.

## Setting it up

There is a F*-Tutorial which comes with an online editor, which is great if you just want to play a bit with the language. You don’t have to install anything, provided you have a recent mainstream browser. The tutorial is fun to do, but after I spent some time on it, I wanted to know what it is like to use F* not on a prescribed path.

Sooner or later, you probably want to install it on your machine, which is not a problem at all, if you are on linux system and an emacs user. There is a binary and an emacs mode which is also easy to install on windows but the combination was somehow forbiddingly slow on my (fast) machine. In the following, pictures will show excerpts from the emacs-mode.

## Programming in F*

Let me first show you, what programming in F* looks like. Here is a definition of the commonly known (higher order) function “filter” which takes a predicate (function to bool in this case) and a list and returns the “sublist” of all things on the list matching the predicate:

The arrows and strange dots are just “->” and “::” rendered by the emacs mode. Otherwise, it is exactly the pattern matching definition that would also work in OCaml or F# (where you can write exactly the same thing):

The second argument “l” is matched against the two things a list might be, either the empty list “[]” or a list with consisting of some first element “x” and a list “xs”. In the first case, we are done and in the second case we decide if “x” should be in the result list and recursively call “filter” to deal with the “xs”.

The type of “filter” can be inferred by F*, but we could have declared it before the definition like this:

The alpha is really fancy emacs-mode rendering for ” ‘a ” and stands for an arbitrary type. This is also the type F* would infer, since what we did does not require anything special from the element type of the lists.

So the declaration says that our function takes some predicate “p” a list of things p may be applied to and returns a list of the same type just with “Tot” written in front of it. The latter tells us, that filter is a total function, i.e. it terminates and will not throw an exception (I guess there is a bit more to it, but so far that explanation worked well for me). There is also a modifier “ML” which would tell us, that the function behaves like a function in OCaml – so it could throw runtime exceptions or loop forever. After introducing you to some verification features, I will tell you why this distinction is important here.

Let us first rewrite our declaration a bit:

I replaced the alpha with a fixed type, the natural numbers (that will simplify things…) and introduced variables “p” and “l” that we can use now to construct types. What kind of types? Well, in this case, I want to construct a replacement for “(list N)” which tells us a bit more about the result of filtering a list. One reason to have types is to make sure, that the result of some construction meets a specification. Usually these kinds of specifications are quite coarse and might just tell you, that the result is an integer. So far, the specification of the filter function only tells us, that the result will be a list of natural numbers. In F*, we can do a lot more. The following specifies the result of filter to be the sublist of all elements of “l” that satisfy “p”:

Between the curly braces, I put a formula in predicate logic, which describes this specification. The ” ” is a logical “and”, the “∀” is the “forall” from math and ” element x l’ ” is some function which evaluates to true if x is an element of l’ and false if this is not the case.

Now, one of the things that make me happy when playing with F* is that the definition of filter I gave in the beginning checks against this new declaration as is. This is due to F* using a problem solver to prove that our specification is satisfied and the not-so-random coincidence that to prove the formula, you can use the same structural induction on the list as we used to recursively define “filter”.

For completeness, here is my definition of “element”:

The “#a:eqtype” means, that “a” is some type such that comes with a total equality function for terms of type “a”. The natural numbers used above are such an “a”. Btw: Those natural numbers are not limited in size, like e.g. “unsigned int”. They behave a lot like “BigInteger” in some languages and are certainly not fast, but they are good for proving things.

And now, I should tell you, that the declaration of “filter” which nicely specified what filter does, is probably not what you should do. In fact, it is usually better to split things into definitions and “Lemma”s. So here is again the original definition of filter (with inferred type) and a Lemma about it:

The “Lemma” is again like “Tot” above – it modifies the type. Technically, “filter_specification” is a function, but the only thing important here, is if its definition (“let rec filter_specification = […]”) type checks with the declaration (“val filter_specification […]”) given – because that means that the definition is a proof of the proposition encoded in the declaration. In particular, it is not important what this function returns. In fact, “Lemma” produces a type all of whose terms are equal.

## Verifying Project Euler exercises

First thing I usually do when checking out a new programming language is to solve a couple of Project Euler exercises to get fluent in the basic constructions. So, I thought, why shouldn’t I try the same with F* and prove something about my solution code?

Problem 1 asks us to add all multiples of 3 and 5 below 1000. Usually, my mind drops the “below” and I get a wrong result. But not so this time! Here is my definition of the natural numbers below 1000, which produces the correct list of numbers, since specifying precisely what it is made me read the problem text very carefully:

Now, “naturals_below_1000” is specified by its type, which turned out to work well in this case, since it is not a general purpose function I will reuse.

Now for the task at hand, we need to filter numbers that are multiples of 3 or 5. I took the liberty to equivalently say, numbers divisible by 3 or 5:

I used modulo arithmetic “%” defined in some library to have an easy definition of “divides”. Also note, that I use definitions in proving that I defined the correct list. Both are a bit fishy if I were to claim that I proved some term in my program meets some mathematical definition commonly used for the concepts in the problem text. So you could call that lazy or efficient according to taste.

Now, the number which the exercise asks for can be defined:

F* can not just check if everything is correct but also evaluate expression. In particular the expression “ex1” which turns out to be the correct answer to the problem.

## Is it of use for the working software developer?

I used Scala some years ago to develop a large prototype and, while there were some pains, it worked about as well as expected and I’m quite sure it would have been less fun and less efficient to use Java for the same project. One important point in the decision to use Scala was the possibility to use Java libraries.
F# has the same kind of advantage and I learned to love its type system from OCaml, which apparently was the basis for F#. So for the same reasons that made Scala work for me when constructing prototypes, I could decide to use F# in similar situations. I don’t know, how realistic my hope is, that F* can be used on top of F# one day, but that would be a great improvement over just having F# which is already something I look forward to. So far, it as possible to extract F# code from an F* program.

Usually, tools like F* are thought of and presented as tools to effectively prevent bugs, i.e. catching all of them no matter the effort. I think, what we need for our daily programming tasks are tools for preventing bugs efficiently. My guess is, that dependent types in a practical language like F# are such a tool. This is of course a heavily biased view, since I have a background involving some dependent type theory, which makes me blind to the effort of learning how dependent types work.

One problem with dependently typed languages is, that small changes can break lots of proofs that took effort to prove. This is particularly bad, if you spell out the proofs in all detail and it means refactoring can become quite expensive.

From what I have seen, the use of a problem solver when type checking reduces this problem quite a bit, so this might not be a real issue here and with other dependently typed languages that do something similar. And of, substitute technologies that achieve similar goals, like unit tests or comments,  also increase refactoring work.

So ultimately, apart from the fun, I also look forward at using F* as tool. As I mentioned before, I already knew about dependent types and could translate what I see when learning F*, so I can’t tell you how much effort it takes, if you don’t already know those things. But what I can tell you is, that learning dependent type theory was certainly among the most rewarding scientific experiences in my life, so maybe you want to do that anyway.

# xBase gotchas

For the last year, I have regularly worked on a legacy project written in xBase / Clipper, which is a dialect of the dBase programming language. The language as a whole is surprisingly comfortable for its age, being 40 years old now. But there were a few quite infuriating things I stumbled upon:

# Trailing commas in arrays

The language allows you to define array contents inline like this:

myArray := { 1, "foo", .t., 4.0 }


It is also dynamically typed, as you can see in this example – where the array holds numbers, strings and boolean (logical) values. Now sometimes, you want to spread-out an array initialization over multiple lines. xBase lets you do that – using the semi-colon quite contrary to many other languages – to continue a line:

myArray := {;
"foo",;
"bar";
}


Now you might be temped, as I was, to write it like this instead:

myArray := {;
"foo",;
"bar",;
}


With a trailing comma. But, gotcha, that does not do what you probably expect. This actually creates an array with 3 elements, where the last element is nil.

# Unequal is not not-equals

xBase has both the == and the != operators. But imagine my suprise when and if a != b was not entered, with what had to be unequal strings. I added some logging (yea, no debugger) and saw that I indeed had the strings "" and "foo". Still, a != b seemed to evaluate to false. Because I could not believe that, I changed it to !(a == b) – and it worked!

It turns out that the != operator is not the opposite of the == operator, but rather of the = operator (xBase uses := for assignment). The = operator, however, implements some kind of “fuzzy” equals by default, also evaluating true if the left operand is a prefix of the right operand. This is a behaviour that can be changed globally by “SET EXACT on”. Wow.

# How to disable IP address logging for Apache web server and Tomcat

The General Data Protection Regulation (GDPR) prohibits excessive or unnecessary collection of personal data. IP adresses in server log files are considered personal data.

Logging of IP addresses is usually enabled by default in fresh web server installations. This article describes how to disable it for the Apache web server and the Tomcat application server, which are a common combination for JVM based web applications.

### Apache Web Server

The apache web server logs the HTTP requests from web clients in log files called *access.log, which includes IP addresses. Another apache log file, which can contain IP addresses is error.log.

To disable IP address logging for Apache edit the main configuration file, usually called httpd.conf and scan it for LogFormat entries, for example:

LogFormat "%h %l %u %t \"%r\" %>s %O \"%{Referer}i\" \"%{User-Agent}i\"" combined

The format ‘verb’ %h stands for the hostname or IP address. This is what you want to remove. You may also want to remove the “Referer” and “User-Agent” components of the log format for privacy:

LogFormat "%l %u %t \"%r\" %>s %O" combined

Restart the server for the changes to take effect.

For Tomcat you have to configure the so-called AccessLogValve in the server.xml configuration file located in the $CATALINA_HOME/conf directory. The configuration entry looks like this: <Valve className="org.apache.catalina.valves.AccessLogValve" directory="logs" prefix="localhost_access_log." suffix=".txt" pattern="%h %l %u %t "%r" %s %b" />  The pattern attribute specifies the log format. Again, the relevant format verb you want to remove is %h for the hostname or IP address:  pattern="%l %u %t "%r" %s %b" />  Restart the server for the changes to take effect. # Clean deployment of .NET Core application Microsofts .NET Core framework has rightfully earned its spot among cross-platform frameworks. We like to use it for example as a RESTful backend for our react frontends. If you are not burying your .NET Core application in a docker container without the need to configure/customize it you may feel agitated by its default deployment layout: All the dependencies live next to some JSON configuration files in one directory. While this is ok if you do not need to look in there for a configuration file and change something you may like to clean it up and put the files into different folders. This can be achieved by customizing your MS build but it is all but straightforward! # Our goal 1. Put all of our dependencies into a lib directory 2. Put all of our configuration files int a configuration directory 3. Remove unneeded files The above should not require any interaction but be part of the regular build process. # The journey We need to customize the MSBuild system to achieve our goal because the deps.json file must be rewritten to change the location of our dependencies. This is the hardest part! First we add the RoslynCodeTaskFactory as a package reference to our MSbuild in the csproj of our project. That we we can implement tasks using C#. We define two tasks that will help us in rewriting the deps.json: <Project ToolsVersion="15.8" xmlns="http://schemas.microsoft.com/developer/msbuild/2003"> <UsingTask TaskName="RegexReplaceFileText" TaskFactory="CodeTaskFactory" AssemblyFile="$(RoslynCodeTaskFactory)" Condition=" '$(RoslynCodeTaskFactory)' != '' "> <ParameterGroup> <InputFile ParameterType="System.String" Required="true" /> <OutputFile ParameterType="System.String" Required="true" /> <MatchExpression ParameterType="System.String" Required="true" /> <ReplacementText ParameterType="System.String" Required="true" /> </ParameterGroup> <Task> <Using Namespace="System" /> <Using Namespace="System.IO" /> <Using Namespace="System.Text.RegularExpressions" /> <Code Type="Fragment" Language="cs"> <![CDATA[ File.WriteAllText( OutputFile, Regex.Replace(File.ReadAllText(InputFile), MatchExpression, ReplacementText) ); ]]> </Code> </Task> </UsingTask> <UsingTask TaskName="RegexTrimFileText" TaskFactory="CodeTaskFactory" AssemblyFile="$(RoslynCodeTaskFactory)" Condition=" '$(RoslynCodeTaskFactory)' != '' "> <ParameterGroup> <InputFile ParameterType="System.String" Required="true" /> <OutputFile ParameterType="System.String" Required="true" /> <MatchExpression ParameterType="System.String" Required="true" /> </ParameterGroup> <Task> <Using Namespace="System" /> <Using Namespace="System.IO" /> <Using Namespace="System.Text.RegularExpressions" /> <Code Type="Fragment" Language="cs"> <![CDATA[ File.WriteAllText( OutputFile, Regex.Replace(File.ReadAllText(InputFile), MatchExpression, "") ); ]]> </Code> </Task> </UsingTask> </Project>  We put the tasks in a file called RegexReplace.targets file in the Build directory and import it in our csproj using <Import Project="Build/RegexReplace.targets" />. Now we can just add a new target that is executed after the publish target to our main project csproj to move the assemblies around, rewrite the deps.json and remove unwanted files:  <Target Name="PostPublishActions" AfterTargets="AfterPublish"> <ItemGroup> <Libraries Include="$(PublishUrl)\*.dll" Exclude="$(PublishUrl)\MyProject.dll" /> </ItemGroup> <ItemGroup> <Unwanted Include="$(PublishUrl)\MyProject.pdb;$(PublishUrl)\.filenesting.json" /> </ItemGroup> <Move SourceFiles="@(Libraries)" DestinationFolder="$(PublishUrl)/lib" />
<Copy SourceFiles="Build\MyProject.runtimeconfig.json;Build\web.config" DestinationFiles="$(PublishUrl)\MyProject.runtimeconfig.json;$(PublishUrl)\web.config" />
<Delete Files="@(Libraries)" />
<Delete Files="@(Unwanted)" />
<RemoveDir Directories="$(PublishUrl)\Build" /> <RegexTrimFileText InputFile="$(PublishUrl)\MyProject.deps.json" OutputFile="$(PublishUrl)\MyProject.deps.json" MatchExpression="(?&lt;=&quot;).*[/|\\](?=.*\.dll|.*\.exe)" /> <RegexReplaceFileText InputFile="$(PublishUrl)\MyProject.deps.json" OutputFile="\$(PublishUrl)\MyProject.deps.json" MatchExpression="&quot;path&quot;: &quot;.*&quot;" ReplacementText="&quot;path&quot;: &quot;.&quot;" />
</Target>


# The result

All this work should result in a working application with a root directory layout like in the image. As far as we know the remaining files like the web.config, the main project assembly and the two json files cannot easily relocated. The resulting layout is nevertheless quite clean and makes it easy for administrators to find the configuration files they need to customize.

Of course one can argue if the result is worth the hassle but if your customers’ administrators and operations value it you should do it.

In the german military forces, there is a new idea coming into effect: Give your commanders the ability to spend free expenses (linked article is in german language). Like, if your battailon lacks sunglasses, you don’t have to wait for bureaucracy to procure them for you (and it probably takes longer than the sun is your immediate problem), you can go out and just buy them.

This is not a new idea, and not a bad one. It implements a simple principle: Resources follow responsibilities. If you have goals to reach, decisions to make and people to manage, you need proper resources. And by resources, I don’t only mean money. Some leniency in procedures, maneuvering space (both real and figuratively) and time are resources that can’t be bought with money, but are essential sometimes.

At our company, we installed this principle over a decade ago. The “creativity budget” is a budget of free expenses for each employee to improve their particular working situation. This might mean a new computer mouse, a conference visit or a specific software. You, the employee, are at the frontline of your work and probably knows best what’s needed. Our creativity budget is the means to obtain it, no questions asked.

And this shows the underlying core principle: Responsibilities follow trust. If I trust you to reach the goals, to make the right decisions and to manage your team, it would be inconsequential to not give you the proper responsibilities. And, transitively, to provide you with adequate resources. As it seems, responsibilities are the middle man between trust and resources.

At our company, you don’t need to invest your free expenses for basic work attire. We are software engineers, so “work attire” means a high-class computer (with several monitors, currently our default is three), a powerful notebook, a decent smartphone and all the non-technical stuff that will determine your long-term work output, like a fitting desk and your personal, comfortable work chair.

For me, it was always consequential that great results can only come from the combination of a great developer and great equipment. I cannot understand how it is expected from developers to produce top-notch software on mediocre or even subpar computers and tools. In my opinion, these things strongly relate with each other. Give your developers good equipment and good results will follow. Putting it in a simplistic formula: the ability of the developer multiplied with the power of the equipment makes the quality of the software result.

So, if I trust your ability as a developer, provide you with premium equipment, give you room to maneuver and resources to cover your individual requirements, there should be nothing in the way to hold you back. And that places another responsibility onto your shoulder: You are responsible for your work results. And you deserve all the praise for the better ones. Because without you, the able developer, all the prerequisites listed above would still yield to nothing.

# There are more exact numbers than you might know

There are lots of annoying problems a programmer can run into, when working with the inexact floating point numbers supported by common cpus. So the idea of using rational numbers

$\frac{n}{d}$

with arbitrary size integers $n,d$ for floating point computation can be quite appealing. However, if you really try this in practice, you are likely to end up with unacceptable performance (for an example, see the post The Great Rational Explosion on this blog).
Another problem with the rationals is, that they don’t support lots of mathematical operations. For example, any prime will not have a rational square root and numbers like $\pi$ and $e$ are not rational.
This post is about the problem of the missing square roots. I will sketch how the rationals can be extended by some specific real numbers. The focus is on what can be done and not how it can be done.

The point of the following example is that we can extend the rational numbers by some new numbers such that we have the square root of 2 and are still able to perform the basic arithmetic operations, i.e. addition, subtraction, multiplication and division by non-zero numbers. And of course, we still want to have the absolute exactness of the rationals.
To achieve this goal, our new numbers can be represented as tuples $(a,b)$ of rational numbers $a,b$. The idea is, that $(a,b)$ stands for the real number

$a+b\sqrt{2}$

And now, a small miracle happens: If you have two of those new numbers then all of the basic arithmetic operations are again given as one of our new numbers! You can believe me or just check this for yourself now. So in total, we have extended the realm of exact calculation to real numbers which are of the form

$a+b\sqrt{2}$.

This is admittedly a bit lame, since we are still far away from calculating general square roots. But the miracle mentioned above is actually not so small and happens in way more generality: The real number $\sqrt{2}$ that we added to the rationals is the solution of the polynomial equation

$X^2=2$ or equivalently $X^2-2=0$

and we can do the same thing with any irrational real number that is the solution of some polynomial equation

$a_n X^n + a_{n-1} X^{n-1} + \dots + a_1 X^1 + a_0 = 0$ or $P(X)=0$

(where $a_n,\dots,a_0$ are rational numbers).
For this general construction, the polynomial above has to be chosen such that $n$ is as small as possible. Then the new numbers can be represented as tuples of length $n$. For the basic arithmetic operations, we think of a tuples $(b_n,\dots,b_0)$ as the polynomial

$b_n X^n+\dots b_1 X^1 + b_0$

and define addition to be addition of those polynomials. To multiply two tuples, take the product of the polynomials and its remainder on division by $P$. You can check out how this recipie does the right thing in the example with $P=X^2-2$. To avoid confusion, let us put the polynomial defining in which extension of the rationals we are into the number. So know, a number is a tuple

$(P,b_n,\dots,b_0)$.

In particular, there are extensions that contain a square root of an arbitrary rational. But if we look at, say, $\sqrt{2}$ and $\sqrt{3}$ we will get two extensions. So we have $\sqrt{2}$ and $\sqrt{3}$ but we can’t do anything that involves both of them. Or in other words, if we have two numbers, $(P,b_n,\dots,b_0)$ and $(Q,c_m,\dots,c_0)$ we don’t know how to perform basic arithmetic unless $n=m$ and $P=Q$.

Here is an easy way to fix this: If we take a step back, we can realize that everything we did above doesn’t need specific features of the rational numbers. The basic arithmetic operations are enough. So we can apply the construction of new numbers including some root to an extension of the rationals. For the problem mentioned above, that would give us tuples of the form

$(X^2-3, (X^2-2, a, b), (X^2-2, c, d))$

– now with four rational numbers $a,b,c,d$.
The corresponding general pattern for an extension (of some extension …) is:

$(P, a_0,\dots, a_n)$

Where the numbers $a_i$ are from some fixed extension and $P$ is a polynomial with coefficients from this fixed extension. We also have to make sure, that $P$ has a property called irreducible. It means that $P$ has at least degree 1 and there is no pair of polynomials $Q,R$ with lesser degree (and coefficients in the extension) such that their product $P\cdot R$ is equal to $P$. If this is not the case, weird things will happen.
Note that if we keep extending our numbers on demand, we can now get square roots of everything, in fact, this even works for square roots of negative numbers. But there are some unmentioned problems, if we want to mix numbers from different towers of extensions. On the other hand, there are also lots of unmentioned possibilites: These construction are pretty general and they can also be applied to finite fields or some extension of the rationals which contains a trancendent element like $\pi$. But I will stop here since my goal of showing some exact representations of numbers that surprised myself once, is reached.

If you want to learn more about the mathematical background, this pdf might help. There is also a way to join two extensions to one of the form we discussed here, the key is this nice theorem: Primitive Element Theorem. There are lots of nice mathematical facts in this area. My former Algebra working group in Karlsruhe, in particular Fabian Ruoff, kindly reminded me of some of them over lunch, when I was discussing the topics of this post.
Then, there are of course implementations. Here is a class in the cgal library for square roots.