Q:

Property based testing without reimplementing the code under test

Given a very simple method such as:
  def squaredDistance(p1: Point, p2: Point) = 
    math.pow(p1.lon - p2.lon, 2.0) + math.pow(p1.lat - p2.lat, 2.0)

What are some valuable property-based tests that don't simply reimplement the method?
I can only think of testing for result >= 0.0, which is pretty broad.

A:

In general, your tests should normally not reimplement the code under test. This can happen to you with traditional tests as well. In fact, from my experience, property-based testing tends to be better for avoiding re-implementations.
When you think about the properties, you specifically do not think about implementation details (i.e. do not think about how you come to some result/property, but instead consider the result/property itself).
Property-based testing is particularly useful for mathematical properties. A square distance function, being quite well-founded in mathematics, is therefore a good match. Nevertheless, it takes a lot of experience. If you have a solid background in mathematics and/or predicate logic, it is so much simpler to find good properties. If all you know is traditional fixed input vs expected output testing, then you are in for a steep learning curve.
So let's look at the function in question a little bit closer. We do have something that works based on Point, so we will need a generator for that - I assume for this answer, that you got that covered already. The resulting value, according to your type signature, is a Double.
First off, property-based tests help you stamp down sub-optimal types. In particular, we know that squared distances always have to be non-negative. A 'Double' doesn't cover that information yet. So there's your first property that you get for free -> limit the result type to more closely resemble the mathematical result domain of the function.
Next, you can look at classical mathematics to find out general relations available for functions/properties and you will come across terms like "(anti-)symmetry" or "transitivity", all of which can be examined to check whether they should hold for your squared distance function. If they do, then you have yourself another well-defined property.
Let's say we add properties to ensure symmetry and transitivity, as well as non-negativeness. Next, you can look at numbers at the border of your domains and realize, that an output of 0 is something special and you add another property for the 0-distance being equivalent to being the same points.
Now you have 4 properties in place already. What I found in my experience of property-based testing is that you often need to make sure that you don't run into this problem: you have defined properties over your domain, but unfortunately, an implementation as simple as if (p1==p2) 0 else 1 satisfies all four properties. 
Why is that? Because all our properties so far concentrated on the input. The output domain of the function is way under-defined still. One way to handle this would again be to add samples (input vs expected output), but can't we find a property for the output domain that does better? 
In fact, some though (aka experience) tells you that when you generate a point, and then generate others, you could argue on the spread of distance values you'll get. You have to be careful to rule out equal points (due to the 0 distance) and the symmetry of distances. (for example, the distance from 0,0 to 1,0 and 0,1 is the same).
There are a lot of possible properties, but let's just make up one example: for each generated point, you use a normal int/double-generator to generate more points that differ in only one coordinate (for example, you start with (3, 15) and generate (3, 4) (3,7), (3,20), ...). When you remove duplicates form these and check the distance from your fixed point (3,15) to all the other (unique!) points, then you know that the distances/results must also be unique. So spoken in a more code-like fashion, you create a set of these other points, not including the fixed point, then calculate the distances for each of these to the fixed point and add the results to another set. Finally, you verify the sets are of equal size. I highly doubt, that your implementation code looks even remotely similar to that.
If you want to be safer, you could add two properties, one per axis (tuple-arity, whatever you want to call it). By adding these properties that essentially describe your output domain as opposed to your input domain, you immediately make it very hard for any hard-coded implementations like the example given above to still succeed.
However, and this is a major point of property-based testing, none of these six properties I have discussed so far guarantee that the actual results of your function resemble the square distance between numbers! So in my experience, you still need a few fixed input vs expected output tests in addition. The cool thing though, is that you can actually get away from your previous preconception that you even need a square distance. Once you start thinking about the actual properties of your functions, you often realize that the even being a "square distance" is nothing than an unimportant implementation detail that you might not even need to care about. So do you just want to have a distance function, or does it matter whether it's squared, euclidean, or something else entirely?
In my experience, if you need to limit it down to the exact function, you need to add in some fixed input vs expected output tests, as the properties in their generality provide still too much freedom. Happy to hear if there's another practical way to deal with this, but as usual, I'm just not seeing a silver bullet here.

