Software correctness made tractable

Syntemantic was founded on the idea that software should behave in accordance with both human-readable and computer instructions. In practice, however, this is not enough, as the assumptions made when working with a computer differ from those used in a formal proof. In recent years, there have been advances in computer-assisted proof languages, so-called "proof assistants", that are able to verify a program using Type Theory, allowing the program to serve as its own proof. For example, many mathematical theorems have already been formalized in the proof assistant Lean, though much progress remains to be made. Unfortunately, not all computer programs can be easily formalized and converted to Lean. We believe that by utilizing well-defined specifications and proper test design, we can use mathematical methods to enumerate an appropriate test suite that matches given criteria. These criteria may differ depending on the type of software; safety-critical systems, for instance, may have stricter requirements than a contact form on a website. By deciding the size and geometry of the test space and constraining it with practical requirements such as time and compute, we are able to make smarter, data-driven decisions when writing software.