Comment by hueving | Hacker News Reader

Comment by hueving | Hacker News Reader

Parent Full thread

Your post contains a lot of unnecessary aggression. Rather than suggesting someone "doesn't know what they're talking about", just provide evidence to the contrary.

That aside, there seems to be something missing in your analysis, or there would be a lot of successful startups stealing the market using proof assistants and formal techniques. It's not anti intellectual to point out that programmers don't want to use academic languages that have poor usability, steep learning curves, and garbage for standard libraries.

Consider when a regular house is being built. There are many problems that could be avoided if an engineering firm spent an entire year analyzing the designs and their interactions with the target site. However, that's not done because it takes significantly longer and costs obscene amounts of money.

It's easier for the construction crew to fix problems as they encounter them and for the owner to do repairs on the house 40 years later. Yeah, the house isn't as reliable, but it cost 100,000 instead of 1,000,000.

If you want developers and managers on your side, you need to show them benefits over the quick development of python/php/Javascript other than bugs in edge cases being less frequent. Don't just bemoan how unenlightened everyone is.

Well, all the naysayers could also do some research instead of being as dismissive as they are. Here's an example of actual use of formal methods: http://lamport.azurewebsites.net/tla/amazon.html Why aren't they used more widely? Because when people hear"math", they immediately think of it as academic. It would also be overkill for most projects.

TLA is one of the systems that are actually very practical. You can go up or down as many abstraction layers as you need . There's a great introduction written by @pron on his blog [1].

However, it's worth pointing out that you don't magically get the final program out of the TLA proof. The proof only works for the abstraction level that you chose to write it at.

[1] https://pron.github.io/

While it is true a full formal proof of a C++ program, for example can take significantly longer and cost obscene amounts of money, that is not true when starting with this approach from the ground up.

There is also a certain level of compromise. By relaxing the requirements a tad, you can still gain many of the benefits while maintaining the light and nimble feel.

So why don't startups use this? Well because there are entrenched technologies that make it very difficult that have nothing to do with the merits of the approach itself.

It is up to us, as developers to take the charge and push for these techniques through open source development, advocacy, and training.

But to claim these techniques are a failure simply because startups aren't using them is pretty ridiculous.

Higher assurance from the start requires something functionally similar to Ada's Spark.

I've never seen that used in the wild (though I'm in the wrong domain (web) these days).

Reply on news.ycombinator.com