Hacker News Reader

Comment by max_ | Hacker News Reader

Yes.

I think programming work in the next decade will be done by logicians using something like TLA+[0] to simply describe specifications.

And something like GitHub co-pilot to translate those specifications to working code.

[0]: https://en.m.wikipedia.org/wiki/TLA%2B

View on HN

At first, i thought you delusional, because make no mistake AI will never make quality software better than a dedicated human (that is until AI is so smart that trying to use it in this fashion is tantamount to slavery).

However... The software doesn't need to be good, just functional. Getting good specs is hard too, but the specs don't need to be complete... I could imagine a terrifying world of startups with very fast "functional" MVPs that are slow as dirt and robust as paper with giant bugs caused by bad specs. It wouldn't be too different from the status quo!

It doesn't need to be AI.

It can just be something from the "formal methods"[0] school of research.

I heard assembly code for CPU's are now days optimized for compilers instead of humans.

[0]: https://en.m.wikipedia.org/wiki/Formal_methods

> AI will never make quality software better than a dedicated human

This seems doubtful given the average quality of human code.

So what you're saying is software will be created by people using some kind of formal notation to write a precise specification for how it should behave, which the technology then follows? If only we had a name for that process...

Exactly, we already do that. We want more detail and control, which means lower-level programming and writing more software.

Specify programs by only a very brief specification is similar to No Code/Low Code. It's great for prototyping and not much more.

This sounds like you're describing 4GLs. That was a popular idea a while ago and it has some echos today, but a lot of that effort died. Outside of very specific scenarios (LabVIEW, maybe crystal reports?), the usage is still minimal. I interact with a single clipper application which I hope gets rewritten soon.

The "your analyst will write your low-code solution" idea is still futurism.

I think it's slowing becoming reality with things like J[0].

[0]: https://en.m.wikipedia.org/wiki/J_(programming_language)

That’s just a different workflow for producing software. What you’re calling a logician here is what most people just call a ‘programmer.’

It's the Law of Leaky Abstractions though isn't it? Most of my time isn't taken by the mainline stuff - it's dealing with things that don't do what they say on the tin or weird edge cases. I'm thinking back to my recent work and really can't imagine any of it being turned into something that could be done in something like TLA+.

> programming work in the next decade will be done by logicians using something like TLA+

How is that not software engineering?

No, TLA+ is not end-to-end. It's describing a toy model only, not the actual programmed system. End-to-end formal methods are completely different.

Reply on news.ycombinator.com