1. 28
muratbuffalo.blogspot.com
1.

2. 11

I also like the converse: If you’re writing a program, use a programming language!

1. 6

The contrapositive is even better. If you are not using a programming language then you are not writing a program.

1. 1

I think you flipped an “ought” to an “is” when you took the contrapositive.

1. 1

Is my language incorrect?

Okay will this then be more clear?

If not using prog. Lang. => not writing program

1. 2

The original statements say how things ought to be, your statements are about how the world is. The proper contrapositive would be “if you aren’t using a programming language, it isn’t true that you should be writing a program.” “if it’s not the case that you should be using a programming language, you aren’t writing a program.”

2. 0

Not true for what most people think of as “programming languages” (or, if you prefer, many programming languages are not obviously so).

2. 4

Not to spoil the article, but the ending quote in bold really sort of scares me. I’ve spent most of my life hearing stories about how machines will take human jobs. The reality of that has played out much less scary (so far) than they’d have had us believe 20 or 30 years ago. It’s never really occurred to me, though, that in another 20 or 30 years that my job as a programmer might be obsoleted as well. It’s like the matrix; funny ha ha, but for real.

Thankfully I hope to be retired 30 years from now :P

1. 4

I think this is the natural progression of things, isn’t it? Programming isn’t immune to the effects of automation - just the opposite, in fact. It’s like boiling a frog - things are automated so often and so incrementally that programmers no longer notice when jobs that would have taken 10x longer a few years ago are basically instantaneous today.

1. 11

Programming will be the last thing to be automated, because it is itself automation - once you have automated programming you just have to run your automated programmer and then you’ve automated everything.

1. 2

…No. The only thing that will save programming from being automated NEXT is… wait, I see what you did there. “Your keys are always found in the last place you look.” :)

On a serious note, regarding future job prospects, I think programming will not be the last available job. Some job that isn’t an attractive candidate for automation will be the last available job. Programming, with all its expense, is a prime target.

1. 4

Once you can automate programming you can automate everything else at approaching 0 cost, so it’s moot.

1. 1

Can you? I would imagine lots of jobs rely on intrinsically tacit, “local” intuition, and not merely knowledge and cognitive function, which is what it seems to me the only thing that “solving programming” entails automatically.

1. 1

Programming often relies on intrinsically tacit, local intuition. I mean think of the last time you received feedback from the customer about how they felt the software should work.

1. 1

Good point I didn’t think about that end of the situation

2. 2

Hopefully, this allows them (and me) to do their (and my) jobs more efficiently, and focusing on other more important things. Of course, other stuff will eventually fall into obsolescence, but don’t we have graveyard keepers, working on decrepit technologies for sizeable amounts of money? COBOL experts, where art thou?

1. 2

All very true. I think the reality just sort startled me.

2. 5

This is why it’s important to move past capitalism ASAP: it’s more and more immoral to couple the ability to get a job with the ability to stay alive and retain dignity. Once all labor is automated, there shouldn’t be any jobs (coerced or obligatory labor), and we should all be rejoicing.

1. 0

Will there still be a free market? Or will what we consume be planned by the machines. At which, point, without the ability to decide what I want - or the illusion thereof - my job as a human is done too …

1. 5

woe to those who think their job as humans is to consume

1. 1

I eat, therefore I am.

2. 1
1. We all make the world;
2. define “free market”.
1. 0

There is a medium of exchange (please not barter) and a market for goods and services. I have goods/services to offer and I have goods/services I need. I have markets to go to sell and buy these. The market is not controlled by the commissariat which determines how much toothpaste I get and what color tube it comes in because for reasons most people can not fathom, I like to chose.

1. 1

you can chose what color tube your toothpaste comes in?

1. 0

In capitalist America, toothpaste color chooses you!

2. 0

What is available in these markets? What is not? How are its dynamics damped, to avoid balloons and crashes? How are negative externalities, like advertising or air pollution, accounted for? You throw around the “free” as though its interpretation were obvious, when the devil is in the details, and the details are everything.

1. 0

This is strawman nonsense, and nowhere do I imply central planning. What you’re really saying is, “I want freedom of choice for consumption and production,” which doesn’t require capitalism, though you’re strongly implying you think it does.

1. 0

You need to elaborate your scheme then. Every time I’ve heard someone say “I hate capitalism and I have an alternative for it” what they really have is state capitalism (AKA communism in practice as opposed to the silly theory of communism written down somewhere).

1. 0

The universal means of production (automated labor), universally distributed.

1. 0

Who decides resource allocation?

1. 0

Who decides it now?

1. 0

The market

1. 0

How’s that workin’ out.

1. 0

Better than anything else people have tried.

1. 0

Citation needed.

1. 0

Also, punch cards were better than anything that came before, and then we had better ideas that were enabled by advancing technology. It’s time we did the same for meeting basic human needs.

1. -1

You haven’t actually said what the replacement is for free markets and capitalism.

1. 0

1. 0

All countries with governments are socialist, not all are democratic, and not all have free markets. So that doesn’t add anything new.

Post-scarcity is another way of saying we have no plan on how to deal with resource contention, which is the hard problem

3. -1

it’s more and more immoral to couple the ability to get a job with the ability to stay alive and retain dignity.

What dignity is possible once you’re livestock to be taken care of?

The truth of the matter is there’s an ongoing demographic implosion. If they wait it out awhile, there won’t be that many people to have to have the universal income or whatever it is you’re arguing for.

1. 3

You’re assuming that dignity and purpose are only possible under conditions of coerced labor. Your premise is false.

I’m not arguing for UBI. I’m arguing for democratic access to the means of universal production (robotic labor, molecular nanotech, etc.), removing the need for things like “income”.

2. 4

My experience is that this is just utterly wrong - I’m not even sure how to start to respond. Of course the best way to express a program fragment is a programming language. Of course the best way to think about a program is with a programming language. There is no distinction between programming and mathematics - of course you want to think mathematically about what you’re constructing, but the best languages for that are programming languages. Why would you want two subtly different descriptions of your program that need to be kept in sync when you could have one description of your program? Some programming languages distract from writing a good expression of your construction by making you specify irrelevant execution details, but the appropriate response is to avoid those languages. A good mathematical description of your algorithm is a program that implements your algorithm, given a decent compiler - and thankfully we’re good enough at those these days.

1. 9

Lobster’s own Hillel expressed it really well just a few days ago:

So many software development practices - TDD, type-first, design-by-contract, etc - are all reflections of the same core idea:

It’s reasonable to want that “plan ahead” stuff to be incorporated in the program (design by contract, tdd), but using an external plan can have a large chunk of the benefit.

1. 6

Maybe, but that’s not an argument for using a non-integrated, harder-to-check plan if you have the option of building the “plan” right into the program.

1. 4

Because there’s design tradeoffs in specification. Integration is a pretty big benefit but also a pretty big cost, often reducing your expressiveness (what you can say) and your legibility (what properties you can query). As a couple of examples, you can’t use integrable specifications to assert a global property spanning two independent programs. You also can’t distinguish between what are possible states of the system and what are valid states, or what behavioral properties must be satisfied.

2. 7

Strong disagree here; you get a lot more expressive power when using a specification language. Let me pose a challenge: given a MapReduce algorithm with N workers and 1 reducer, how do you specify the property “if at least one worker doesn’t crash or stall out, eventually the reducer obtains the correct answer”? In TLA+ it’d look something like this:

(\E w \in Workers: WF_vars(Work(w))) /\ WF_vars(Reducer)
=> <>[](reducer.result = ActualResult)


Why would you want two subtly different descriptions of your program that need to be kept in sync when you could have one description of your program?

I’ve written 100 line TLA+ specs that captured the behavior of 2000+ lines of Ruby. Keeping them in sync is not that hard.

1. 9

I’ve written 100 line TLA+ specs that captured the behavior of 2000+ lines of Ruby. Keeping them in sync is not that hard.

Keeping code in sync with comments that literally live along side them is even more “not that hard”, and yet fails to happen on an incredibly regular basis.

In my experience, in any given system where two programmer artifacts have to be kept in sync manually, they will inevitably fall out of sync, and the resulting conflicting information, and confusion or mistaken assumption of which one is correct, will result in bugs and other programmer errors impacting users. The solution is usually to either generate one artifact from the other, or try to restructure one artifact such that it obviates the need for the other.

1. 4

Keeping code in sync with comments that literally live along side them is even more “not that hard”, and yet fails to happen on an incredibly regular basis.

The difference is that if your code falls out of sync with your comments, your comments are wrong. But if your code falls out of sync with your formal spec, your code probably has a subtle bug. So there’s a lot more instutional pressure to update your spec when you update the code, just to make sure it still satisfies all of your properties.

The solution is usually to either generate one artifact from the other, or try to restructure one artifact such that it obviates the need for the other.

This has been a cultural problem with formal methods for a long time: people don’t value specifications that aren’t directly integrated into code. This has held the field back, because actually getting direct integration is really damn hard. It’s only in the past 15ish years that we’ve accepted that it’s alright to write specs that can’t generate code, and that’s why Alloy and TLA+ are becoming more popular now.

1. 6

What justifies that assumption. Some junior will inevitably, in response to some executive running in with their hair on fire over some “emergency”, alter the behaviour of the code to “get it done quick” and defer updating the spec until a “later” that may or may not ever arrive. Coming along and then altering the code to meet the spec then re-introduces the emergency situation.

The fundamental problem here is that you’ve created two sources of truth about what the application should be doing, and you cannot a priori conclude that one or the other is always the correct one.

1. 6

And what happens when that “emergency” fix loses your client data, or breaks your data structure, or ruins your consistency model, or violates your customer requirements, or melts your xbox, or drops completed jobs?

Yes, it’s true that sometimes the spec needs to be changed to match changing circumstances. It’s also seen again and again that specs catch serious bugs and that diverging from them can be seriously dangerous.

1. 2

And what happens when that “emergency” fix loses your client data, or breaks your data structure, or ruins your consistency model, or violates your customer requirements, or melts your xbox, or drops completed jobs?

Nobody’s arguing that the spec is useless, just that the reality is that it does introduce risks that require care and attention and which cannot be handwaved away with “keeping them in sync is not that hard” because sync issues will bite organizations in the ass.

2. 2

It’s only in the past 15ish years that we’ve accepted that it’s alright to write specs that can’t generate code, and that’s why Alloy and TLA+ are becoming more popular now.

It would be very helpful if you could at least generate test cases from those specs though. But then that’s why I work on a model based testing tool ;)

1. 2

Which one?

1. 3

Proprietary of my employer (Axini). Based on symbolic transition systems, a Promela and LOTOS inspired modeling language and the ioco conformance relation. Related open source tools are TorX/JTorX/TorXakis. Our long term goal is model checking, but we believe model based testing is a good (necessary?) intermediate step to convince the industry of the added value by providing a way where formal modeling can directly help them test their software more thoroughly.

1. 2

Really neat stuff. Thanks. I’ll try to keep Axini in mind if people ask about companies to check out.

1. 2

Thanks, I’ve also been regularly forwarding articles and comments by you to colleagues :)

1. 1

Cool! Glad thry might be helpig yall out.:)

3. 2

This was a problem in high-assurance systems. All write-ups indicated it takes discipline. That’s no surprise given that’s what good systems take to build regardless of method. Many used tools like Framemaker to keep it all together. That said, about every case study I can remember found errors via the formal specs. Whether it was easy or not, they all thought they were beneficial for software quality. It was formal proof that varied considerably in cost and utility.

In Cleanroom, they use semi-formal specs meant for human eyes that are embedded right into the code as comments. There was tooling from commercial suppliers to make its process easier. Eiffel’s Design-by-Contract kept theirs in the code as well with EiffelStudio layering benefits on top of that like test generation. Same with SPARK. The coder that doesn’t change specs with code or vice versa at that point is likely just being lazy.

2. 3

Why would you want two subtly different descriptions of your program that need to be kept in sync when you could have one description of your program?

For example to increase the number and variety of reviewers and thus reducing bugs.

A good mathematical description of your algorithm is a program that implements your algorithm

Are you thinking of a specific compiler? I agree that programmers think mathematically even when they use programming languages to express their reasoning, but I still feel some “impedence” in every language I use.

1. 3

For example to increase the number and variety of reviewers and thus reducing bugs.

That seems very unlikely though. Even obscure programming languages are better-known than TLA+. More generally I can’t imagine getting valuable input on this kind of subject from anyone who wasn’t capable of understanding a programming language. I find the likes of Cucumber to be worse than useless, and the theoretical rationale for those is stronger since test cases seem further away from the essence of the program than program analysis is.

Are you thinking of a specific compiler? I agree that programmers think mathematically even when they use programming languages to express their reasoning, but I still feel some “impedence” in every language I use.

I mostly work in Scala so I guess that influences my thoughts. There are certainly improvements to the language that I can imagine, but not enough to be worth using something other than the official language when communicating with other people.

3. 1

He assumes that machine learning will not also change mathematics. This is baseless.

1. 1

yeah at least in ML you could tell your model that 1=2, or if you really want to be embarrassingly on the nose, 2+2=5

1. 1

Just like parallel lines meet in infinity in physics? Models are useful, but not the Truth with a big T.

2. 0

Agreed: software is always mathematical text interpreted by a machine.
And just like any other human texts, it can be wrong. Thus any tools that force humans reviews is very useful.

Algorithms are not programs, and they can be expressed in a simpler and more expressive language. […]
imagine trying to discover Euclid’s algorithm by thinking in terms of code rather than in terms of mathematics.

IMHO, Euclid himself did not discovered the algorithm by using the “terms of mathematics”, but by using the “method of mathematics” (a method that actually is mathematics).
The notation was not that important and indeed the language of math depends on the mathematician who is speaking.

Maybe this is the curse of the Whorfian syndrome Lamport wrote about in another article. “Computer scientists collectively suffer from what I call the Whorfian syndrome – the confusion of language with reality.”

Like when they talk about “machine learning” and “artificial intelligence”? :-D