Do tagless algebra needs laws?

I read the wonderful blog from JOHN A DE GOES regarding to tagless final. In the section 5.Fake Abstraction, he has mentioned:

Unfortunately, these operations satisfy no algebraic laws—none whatsoever! This means when we are writing polymorphic code, we have no way to reason generically about putStrLn and getStrLn.

For all we know, these operations could be launching threads, creating or deleting files, running a large number of individual side-effects in sequence, and so on.

He is correspond to the following tagless algebra:

trait Console[F[_]] {
  def putStrLn(line: String): F[Unit] 
  val getStrLn: F[String]
}

Does it mean, writting laws for tageless algebra is not possible or do I misunderstand something.

A few things:

• John A De Goes, while is very knowledgeable has also a lot of opinions and express them as if they were inferred from mathematics without making a clear distinction - this posts is a part of series where he basically pitches that tagless final is often a bad solution and ZIO is a good one
• paragraph says that tagless final often doesn't follow algebraic laws which means that we cannot e.g. consider IO monid/semigroup and similar. Which is true. But it doesn't mean that these constructs cannot obey some contracts (called laws) because the do and that is the whole point of Cats Effect
• nobody can force you to write laws for algebras, because laws are basically some particular way of writing specification/tests where you write a separate test for some class of interfaces and then for every implementation you can instantiate this test to check if your implementation fulfill contracts - and yes, nobody can force you to write test for your code. However, that can be said about virtually everything we code, and TTFI give you benefit of making it easier to specify a common behavior of widely different implementations, and then writing your code and tests carefully, sticking to the part of contract that is vital for a particular piece of code while also making these dependencies on contracts explicit

So yes, nobody can force you to write laws for your algebras, but people who implement them in libraries actually do this, and if you write your own algebras, you are encouraged to do so, so this argument is stretched and eristic.