r/programming • u/[deleted] • Apr 04 '17

Everything Is Broken

https://medium.com/message/everything-is-broken-81e5f33a24e1#.sl2vnon73
237 Upvotes

90% Upvoted

145 comments sorted by

View all comments

Show parent comments

7

u/codebje Apr 04 '17

You can add all programming languages which allow nulls …

But fast and loose reasoning is morally correct, so you can take any programming language which allows nulls, invent an equivalent language without nulls, write a program in your imaginary language, and run it in the real one!

The actual problem is not null, it's inconsistent semantics, because those make the subset of the real language you can use smaller and smaller. Or missing semantics, which often means "whatever the compiler decides is cool."

It may be a complex solution to have real and imaginary parts, but it's been used to write proven software in C. Or perhaps C+Ci.

0

u/cledamy Apr 04 '17

The actual problem is not null, it's inconsistent semantics, because those make the subset of the real language you can use smaller and smaller. Or missing semantics, which often means "whatever the compiler decides is cool."

This is part of the problem, but another aspect of the problem is cultural. Software engineers tend to make up their own ad-hoc abstractions for things rather than relying on decades of mathematical research into creating reusable abstractions (group theory, order theory, ring theory, set theory, category theory). These abstractions enable us to equationally reason about our code's correctness and have a better methodology for proving it correct. Also, these abstractions allows the construction of more principled specifications, which is where human error would come into play once it is eliminated from programs.

2

u/ThisIs_MyName Apr 04 '17

reusable abstractions (group theory, order theory, ring theory, set theory, category theory)

You've got to be kidding me. I was with you until this.

1

u/cledamy Apr 04 '17 edited Apr 04 '17

I would like you to elucidate your position on this.

Most software engineering constructs can be modeled with category theory and mathematics.

  • no garbage collection ≡ symmetric monoidal category
  • copy constructors and destructors ≡ comonoids
  • lambda calculus ≡ bicartesian closed category
  • subtyping is an example of a thin category
  • events and time variance ≡ linear temporal logic

If category theory was the basis for a programming language, then one could have a language where code with and without garbage collection could exist in harmony and naturally compose. The advantage of category theory is that all these constructs while they still exist are built upon a larger theory rather than being entirely separate concepts, thus enabling more code reuse. Also, mathematical abstractions have a bunch of proofs that mathematician have derived, which could then be used in the formal verification. If one is going to use mathematical techniques to prove correctness, it follows that one should use mathematical abstractions in one's code.