[Ferret7446]

> Program correctness can be proven.

It can be proven, in broadly the same sense as all of the atoms in your body can simultaneously "decide" to exist an inch to the right due to quantum field theory.

It is not practical to prove correctness for the vast majority of programs, and there are programs that are demonstrably incorrect, cannot be made correct, and yet are useful and still function anyway (e.g., closing TCP connections cannot be done "correctly").

[hulitu]

> 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.

[strken]

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.

[VBprogrammer]

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.

[meoleo]

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.

[AtlasBarfed]

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?