Ari's Questions

• What is apropos? Is it property testing? Does it supercede property testing? Does it supercede unit testing? What work does it do for you? What work do you need to do?

  Apropos is a tool for meta-programing property tests based on logical models. Apropos will solve the model and generate the appropriate tests to verify the model. You need to define the properties, the model of their logical relationships, how to test each of them, some runner for your scripts, and a logical formula for when that runner should succeed.

• What does apropos give me over ordinary property testing? Is it easier? More comprehensive? Does it write tests for me? What do I need to tell it?

• How does apropos compare to distortion/mutation testing? Is it similar? What are the advantages?

  The HasPermutationGenerator can be thought of as mutation testing. A PermutationGenerator is defined as a set of random Morphisms that "mutate" the underlying type from an inhabitant that has some set of properties to an inhabitant that has a different set of properties. These Morphisms are like dependently typed mutations. When these Morphisms form a strongly connected graph between all of the partitions defined by the logical model for a type we can use them to generate an inhabitant of the type for any partition.

• The README discusses generating and running property tests. My understanding is that apropos is implemented built on top of Hedgehog property testing, but is not equivalent to property testing, but rather goes beyond property testing into more comprehensive, quasi-formal verification-type testing. Is this correct? If so, mention of property testing seems misleading.

• What is the role of generators in apropos?

  Generators in Apropos are like random generators that you are familiar with. The difference is Apropos cares about being able to generate things that satisfy some set of properties. The HasParameterisedGenerator class encapsulates this - we need to build a generator that can - given a set of properties generate an inhabitant of the underlying type that satisfies this set of properties.

• My understanding is that apropos follows the style of formal verification. Exhaustively checking these models would amount to full formal verification (To the extent of the specification) but this is computationally unfeasible, so apropos randomly runs tests to probablistically build confidence in the model and code. Is this correct?

• What does it mean for my code to have a logical model? Is it a formalization of something I already have in my head? Do I need to formalize something further? What does such a model look like? How does it compare to a set of property tests? Must it be comprehesive or can it be partial?

• The logical model is split over several compoents - the propositions type, the logic method of LogicalModel, the satisfiesProperty method of HasLogicalModel and the definition of the generators. What do each of these do? How do they interact? Is there any duplication within these or with the code?

• What code is being tested? Taking IntProp as an example, is the integer representation? The comparison logic in satisfiesProperty? The comparison logic in HasPureRunner?

• What does it mean to test model consistency?

• I know I need to define a set of propositions. What are those propositions? How do I choose them? The proposition type in the integer example is a pure sum type. What would it mean for this type to have a more complex structure e.g. fields?

• Does the choice of propositions affect the distribution of test cases?

• How does apropos devise negative test cases? How can I be confident these are exhaustive enough?

• What does the graph in HasPermutationGenerator represent? How is it used?

• In the integer examples, how is the permutation example equivalent to the hand-written one? What is the advantage, or concept being demonstrated? It seems rather more complex.

• Is there (or could there be) a way of automatically generating generators, like Hedgehog itself does?

• apropos currently works by generating single values. Does it make sense to extend this to multiple function inputs? (You con do this with a product type, but it's not very composable)