> but we managed to declare 1 part of the state correct, and derive all the other state from it

Isn't this the essential philosophy of React?

The other approach is INotifyPropertyChanged-style: an event for every change, which is supposed to propagate to all listeners, but only propagate if the value is different. It sounds like this is the one that had failed in the project you were given.

> Typing 3 characters would enable or disable most GUI elements 3 times

I don't think this matters so long as you can coalesce all the redraws. See also "immediate mode" GUIs: if you always redraw everything from the canonical state, which modern computers are extremely fast at, a lot of complexity goes away.

> it was too late to make invalid states unrepresentable

It wasn't, that's exactly what you did, albeit not with types, but by removing redundancies from the state. It's the same reason why normalizing relational databases is a good idea.

Very nice!

This is the essence of model, view, controller, and also one of the very first use cases for it!

Take a look at Ada sometime, it really takes that to eleven.

   type Digit is range 0 .. 9;

   type Unsigned_Byte is mod 2 ** 8;

   type Binary_Floating_Point is digits 15 range -1.0 .. 1.0;

   type Binary_Fixed_Point is delta 2.0 ** (-32) * Pi range (-Pi / 2.0) .. (Pi / 2.0); 

   type Decimal_Fixed_Point is delta 0.01 digits 5;

Yes, this was a really nice advantage Pascal had that I'm amazed hasn't been picked up by things like C#. It's not just zero or one based.

(It's been long enough I'm not completely sure of the syntax) Time : Array [2000..2100, 1..12, 1..31] of OneDayInfo;

Avoid allocating the 2000 years in the past while allowing directly indexing with the year field.

And you could use enum types as array indexes. In C# you're always casting them to int whenever an enum is an array index and every cast is a case where the compiler won't have your back in hunting for errors.

And it did *not* use duck typing.

Month: 1..12 DaysOfChristmas: 1..12

You couldn't assign which day of Christmas to a month.

The stricter the compiler the fewer bugs will even compile and the faster you'll find the problem.

As for his color assignment issue--you still need to be able to set it to "purple", but representing it his way pushes this back to whatever routine parsed the configuration. There's only one place that needs to make the check and anything bogus will be caught during startup.

One really nice thing about object pascal(and nim I think) is that you can declare enums as array indexes.

  type
    TMonth = (mJan = 1, etc);

    TFooPerMonth = array[TMonth] of integer;

Nim smells like a modern Pascal sometimes, and it has this feature as well.

If I could just have an enum restricted to the enumerated values, I'd be happy. It's pure insanity that even a c++ enum class can take on an integer value.

Forth is tic-tac-toe and dependent typing is global thermonuclear war.

I love that, going to reuse that one

Why should math trigger an alarm in engineer's mind? The only thing that triggered my alarm is that it's a pretty bad math - why thinking in terms of cardinalities when we are really talking about subsets? And why use ℝ - which is an agreed symbol for a set of real numbers - for anything else than that?

We use math in all kinds of professions and in everyday life, it's a perfectly valid way of explaining the concept I think.

> The less out-and-out math used to make a point about programming, the better, I think.

Curry and Howard have some bad news for you https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

I second this as I find that usually the solution that is the most mathematically pure is usually also the one completely inadequate at handling the complexities of real-world applications and end up having various extremely impure additions bolted onto them (as shell scripts or Excel spreadsheets on a shared network drive if necessary) because refactoring them into an equally pure solution for the real-world case would take too long.

> The less out-and-out math used to make a point about programming, the better, I think.

Imagine if an electrical engineer said this. Or an aerospace engineer. Or any real engineer.

I would say it's a tool with an optimal point that is located along the "heavy use" side. I think it is interesting to think of them as solidifying your specification. As such if your spec is still changing or it is unclear (e.g. first impl draft, example code...), you should use some lightweight types, whereas a public API should have types that encode basically everything your comments can say about the values, operations, and memory representation of the parameters. That would be the point where I would consider that defining my types is "done" and I would consider switching to e.g. moving the functiona around instead (there are lots of hanging fruits in safe by construction approaches, that might not even require types - can't shoot yourself in the foot if I remove the footgun entirely)

Invariants need to be encoded one way or another anyway, you can't escape that. If your type system is not sophisticated enough this gets tedious and awkward to do in the type system, so it's easier to do in (dynamic) code. But dependent types simplify this, they make it much easier to express yourself in types compared to, say, all the various fancy extensions to System F. Computing types becomes just like computing terms.

That said, there is a vast design space between Javascript/Python and dependent types. Plain old ADT suffice in 95% of cases, yet the only mainstream language with ADTs is Rust. This is a shame.

There’s no shame in just having complex constructors to check some invariants in non-structural ways. At least you still capture and enforce the transition.

   record Point(double X, double Y);

   record Point {
      public required double X { get; set; }
      public required double Y { get; set; }
   }

I've come out of a job of spaghetti and idiots.

My team lead used to shoot down ideas if they were "too complex". Correct and wise, right?

Except that this numskull created reams of functions that took untyped python dictionaries, did something, and passed them to other functions.

Early on, he bolted a giant mess of validation onto the perimeter. This did add value... but most data invalidity arose inside the fucking app!

He had a great eye for the complexity of abstractions, but was completely blind to the complexity of doing simple things in convoluted ways.

It was miserable. Any random PR could pass all the integration tests we had and still blow up prod, because there were orders of magnitude more code paths than lines of code.

The abstract concept here is liveness, aka "eventually something good will happen". In practise, liveness alone is insufficient because a locked up program/processor is indistinguishable from a very slow program/processor. So you really want bounded liveness, along the lines of "within X time units, something good will happen".

This sinks so many "business transformation" projects, especially in the public sector. An organization contains explicit knowledge, which is written down in its processes, and tacit knowledge, which isn't, and may not be known to managers! But when converting a business to software the tacit knowledge, critical to the functioning of the business, gets lost.

I would argue that languages are not ready for perfect information representation. Programs explode when presented with minor inconsistencies. And changing the representation in minor way requires rewriting the program.

With CUE, we are trying to solve this exact problem.

Do you think "state machines" should be called "data machines"? Why or why not?

IMO "state" is a better fit for the concept that this is getting at. The point is to stop the program getting into an invalid state, not to stop the program operating on invalid data, because a program might need to process data that's invalid in some sense, and because the program state is something a bit more active than "data" (e.g. having the right data at the wrong stage of execution is also an invalid state, even though it isn't exactly "invalid data").

The way I understand it, "state" refers to any point in time during the execution of a program.

A computer program can be split into 3 large parts: input, process, output. And invalid data, in my opinion, only concerns the first part, whereas invalid states can be found throughout all parts of the program due to e.g. bugs.

That makes "make invalid states unrepresentable" more generic than "make invalid data unrepresentable". Or to put it in another way: invalid data can lead to invalid states, but not all invalid states are due to invalid data.

State is a collection of values. Data is a single value.

A checkbox represents a single value. A collection of checkboxes represents something different, the state.

"State" alludes to "state machine". It's natural to refer to inputs and outputs as "data", and they are definitely not "state", but the thing in the middle while processing the data? That's state, including things like the file pointer and the lexer state machine which are not part of the "data".

You can actually get quite some way by adding constraints to columns. NOT NULL, default values and a CHECK constraints on a column can limit random invariance bleeding into the db.

So for example, if I ever see a CHAR(1) column that looks like it's meant to hold a boolean of some sort, the best thing is to immediately lock it down to a strict subset (preferably not NULL) of 2 states like ['Y'|'N'].

I still have nightmares about a db schema that grew a fungus of boolean representations, and massive amounts of code checking for y,n,Y,N,0,1,T,F,t,f all of which were used by different teams at different times. Constraints would have stopped all that.

Here's the docs for Postgres: https://www.postgresql.org/docs/current/ddl-constraints.html

As the sibling post says, constraints can cover a lot of this already. What I'm not sure about is how applications querying the language would interact with a database that provides a lot of useful invariants natively; if the application language's type system can't express those invariants, I think you'd end up with impedance mismatches that could cause a lot of frustration.

I've had some idle thoughts about creating a Postgres extension that would make some of these concepts easy to implement and work with. I modeled a sum type/discriminated union a while back, I was able to make it work with constraints, but it was fairly verbose.

  struct AdminNote {
      id: String,
      text: String,
      category: CategorySpecificData,
  }

  enum CategorySpecificData {
      GeneralRequest,
      InitialRequestForm {
          appliesToBasicRequestDetails: bool,
          appliesToSubjectAreas: bool,
          appliesToAttendees: bool,
      },
      SupportingDocuments,
      ConsultSession,
      AdviceLetter {
          appliesToMeetingSummary: bool,
          appliesToNextSteps: bool,
      },
  }