Hacker News Reader

Comment by auggierose | Hacker News Reader

None of these languages represent the medium term future, but are certainly interesting milestones along the way that will inform it.

The real future though is theorem proving systems, and generating code from them. I don't mean so much Agda, Idris, etc., which try to approach theorem proving from a programmer's point of view. But theorem proving systems that embrace the full spectrum of abstract and correct thought.

Zig and Rust try to get there without paying the heavy price that theorem proving incurs (Rust pays that price more than Zig already, though). But to truly progress we need to pay that price and make it lower and lower with time.

View on HN

> The real future though is theorem proving systems, and generating code from them.

I've heard the same thing about model-driven development 25 years ago. Outside of some very small niches, it's pretty much dead now.

> But theorem proving systems that embrace the full spectrum of abstract and correct thought.

And here's where reality and the ideal world collide: the vast majority of applications consists of incomplete models (in that data and/or understanding of the problem are incomplete), quickly shifting goals, and pressure to release.

Theorem proving systems offer nothing that helps with this class of software - abstract and correct thought sounds marvellous in an academic environment or if you have unlimited budget to hire top talent and perform thorough analysis.

In practice, however, your typical line-of-business application is faster, cheaper, and well-enough programmed using traditional languages and a healthy dose of best-practises.

Optimisation and platform support are another area where a TPS won't be very useful. Every hardware has its quirks and workarounds are required to get the best performance or avoid pitfalls. These aren't easily expressed (and identified) using abstract thought and models.

Last but not least, no sane company is going to just throw away decades worth of investment in applications, libraries, and (software-)infrastructure just for a nebulous promise of what basically boils down to smarter and better staff with the right tools.

Theorem proving systems have their place and that place might get bigger in the future, but they're most certainly not the panacea of all software development.

The "generating code from them" brings the bad vibe of useless UML tools with it, but I put it in there anyway, because that's how it is going to be.

There is room for "experimental" programming of course, where you experiment with stuff and you are glad that you get it somehow working in the first place. But should stuff that peoples lives depend on depend on experimental software like that? No. And as software more and more becomes part of our lives, I don't see much software for which that attribute does not hold.

Same goes for hardware.

Could you elaborate or illustrate what you mean by "theorem proving systems that embrace the full spectrum of abstract and correct thought"?

As a mathematician (and programmer on the side) who regularly works in Coq, my impression is that Rust does represent "the future of programming" (or rather, my ideal of it). Type systems are the only mechanism (that I know of) for formally ensuring properties of programs, and proof assistants and languages like Rust lie on two extremes of the spectrum. The former puts the type system in focus; indeed all my work in Coq is about convincing the compiler that certain functions (terms) type-check. The latter puts types in the background, trying to prove as much as possible with minimal friction.

What's the alternative?

Very interesting, I don't know many mathematicians working in Coq. What is your field?

My work is related to homotopy type theory. There are mathematicians working in Agda and Lean (2, but also 3) as well, but it certainly is a niche field.

Ah, makes sense. By being able to express "abstract and correct thought" I mean being able to express myself in a system much like a mathematician would. Coq for example is too constructively oriented for my taste to make that possible (I know, you can "just add an axiom" ...), and its automation is also (therefore?) not good enough.

Would love a real programming language where one can write subroutines and structures that are directly checked for logical correctness and performance. Having to rewrite something in an alternative language to prove correctness is a major pain.

Reply on news.ycombinator.com