Tachyus is Hiring a Correctness Engineer
At Tachyus, we don’t believe that the title “quality assurance” is specific enough. The most fundamental characteristic of good software is correctness: the adherence of the product’s appearance and behavior to the vision that inspired it. We are hiring a Correctness Engineer to lead our internal effort to build and deliver software that is, above all, correct. This person will share our belief in the following principles, and help us apply them comprehensively.
The Correctness Engineer’s Manifesto
Enumerate facts rather than instructions
In functional programming, complex behaviors are achieved by composing facts rather than manipulating data. As a simple example, consider the functional, recursive implementation of the factorial (in F#) and its imperative analog (in C#).
an enumeration of facts
In the functional version, we just have to state two facts about the nature of the solution we want. On the other hand, the imperative version tracks two changing states (the values of the index and the “result”) and gives instructions for how to manipulate them until the result is achieved. To show that the latter is correct, we have to reconcile the instructions with the problem definition. For the former, the implementation essentially is the problem definition.
Let the type system do the work
The more robust your type system, the more bugs you can catch before you even compile your code. F# has a particularly strong type system that enforces correctness in a number of unique ways. Floating point numbers and integers can be given units of measure that, when included in arithmetic expressions, eliminate a whole class of potential errors.
Type providers provide another powerful extension to the type system, providing safety across interfaces with external data sources. For example, the SQL command type provider enforces the matching between types in code and table schemas in SQL databases.
Compile specifications to tests
Specs can be valuable, but they are useless in the case that they are written ambiguously or ignored. If every specification is programmatically compiled to a set of test cases to be executed, both of these problems are eliminated. Using the Gherkin language, a “business readable” domain specific language, we can ensure that each specified behavior is defined clearly in terms of inputs and outputs. The given-when-then pattern is checked and defines the inputs, steps, and outputs of an acceptance test. As an example, the Gherkin specification below, together with its implementation in TickSpec, allows it to be run and checked automatically.
Don’t just test the code — prove the code
The ML family of languages has its roots in automated theorem proving — the study of software that can explicitly verify mathematical proofs. The same principles can be applied to verify the correctness of programmed algorithms. The assertion that a program is correct because a certain set of test cases pass is usually a fallacious proof by example, whereas formally proven programs are correct by logical deduction.
Correctness is not a platonic ideal, but is instead defined with respect to a concrete specification. Accordingly, proof of correctness requires a thorough and highly formal specification. As an example, miTLS is a real-world application that is formally proven to be correct against its specification (which was written in F7, a sibling language of F#).
Prefer automated, deterministic, idempotent processes
The constant change that a production software system undergoes as it grows can be an enormous risk if mismanaged. Builds and deployments can introduce issues if they are ambiguously defined. Haphazard data migration can lead to schema inconsistencies or data loss. Manual tests can have vaguely defined notions of “passing”. When all processes are automated and repeatable, a product measured to be correct will remain correct. Thus far, we have had great success defining processes with FAKE and automating with Appveyor.
Join Us
If you appreciate these principles, and want to help us innovate in the science of building and delivering correct software, let us know at jobs@tachyus.com.
