Hacker News new | ask | show | jobs
by hulitu 513 days ago
> It is not practical to prove correctness for the vast majority of programs,

That is the excuse i hear a lot from software developers, when everything they do is to test the expected behaviour of a program, without any edge case.

And this is also the reason why iMessage and WhatsUp are full of one click exploits.
2 comments
strken 513 days ago
The comment you were replying to is about formal proofs of correctness, probably using tools like Rocq (formerly Coq) and TLA+.

These tools can take an extreme amount of time to use and require specialised skillsets that are difficult to hire for. They go far beyond standard software engineering practices like unit and E2E testing. It is genuinely, seriously not practical to verify the average startup's SaaS web app with TLA+; you'd go bankrupt.

Someone who's used them more than me might be able to comment on exactly how hard it would be, but I felt it was unfair to you not to explain.

link
VBprogrammer 513 days ago
It is possible that the person you replied to wasn't confused by that. I've certainly come across the type of developer who'd deride the lack of ability to formally test their code then, in the next breath, click through the happy path of their code and send it.
link
meoleo 511 days ago
TLA+ and Coq are too hard for most SAAS applications. Tried FizzBee (https://fizzbee.io/tutorials/getting-started/) and P (https://p-org.github.io/P/whatisP/)? These seems quite practical.

Coq/Rocq are obviously much harder to use, and I mostly see embedded systems engineers use them. TLA+ is somewhat easier, and being used in a number of cloud infrastructure companies (AWS, MongoDB, Confluent etc).

Obviously, if you are building a simple CRUDL app, these tools don't help at all.

link
AtlasBarfed 512 days ago
Oh yeah, just prove it correct. Simple

Wait, code is not simple. Are the requirements simple? Oh wait, in reality they aren't simple either.

The complexity of the formal specification must ramp up with the complexity of the code, because the task being asked is complex.

So where does the debugging end if the specification is wrong?

How do you prove the requirements are correct?

Unit testing is helpful but wasn't the panacea, because the most important bugs are in integration.

I'm also going to guess that formal proofs will have hellacious issues with system boundaries. They can't prove correctness of the state on the other end of the pipe.

So you overcome that, time and money. What happens when the requirements/specification changes? How much of the verification is invalidated?

Proof systems need to prove their economic validity in the he software realm. Heck, where are the proof systems for subsections of the Linux kernel or other vitally important inner loops of computing? Those actually have stable specifications. Weren't go multitasking formally verified/provably correct in some sense? Why haven't correctness tools tackled other things?

link