On Determinism (Compiler Driven Development)
TLDR; its usually better to model software close to mathematics in order to keep it deterministic and testable
On maths and software engineering
Software engineering is no doubt a branch of mathematics but since its also a language which means it brings subjectivity, this tends to make it ambiguous in lot of situations. But it does help going back to the roots of programming that is maths and little exploration will bring clarity into how much of it has actually been always driven by maths.
Algebraic Data types
Regular language constructs like enums, structs and classes or even a primitive type like Boolean has always been closely associated with algebra on the way they were constructed.
For example, Boolean is type with 2 possible values, Never type has 0 possible value or Void has a 1 possible value
Choosing Booleans in a struct creates a product type with 2*2 = 4 possible type values and 3 booleans would make it 2 * 2 * 2 = 8 types, hence structs are product types. Maybe some of the values are never cared by the if-else conditions.
Maybe its better to use enums that model discrete types which can be counted as per cases added hence enum are sum types.
This concept is very important for subsequent analysis of how compiler can generate proofs for a program.
WIP (I want to write this article properly)
Here are topics I will expand on
- Parsing over validating
- Type state pattern using non consumable types and borrow/consume constructs
- Type driven algebraic domain modeling
- Boolean blindness by Bob Harper
- Functional programming constructs
- Falling into Pit of success by Jeff Atwood
- Compiler proof as first step in testing triangle over unit tests