News for hackers. Stuff that matters.

A comment on I interviewed Brian J. Fox, the creator of Bash. Parent comment

Re:I interviewed Brian J. Fox, the creator of Bash by SavantIdiot on Thursday September 02, 2021 @02:43PM (#28395766)
"I don't think I have ever run into a bash bug or issue."

That is not a statement about a formally verifiable program that I would base a billion-dollar program on.

[ Parent | on HN ]
Re:I interviewed Brian J. Fox, the creator of Bash by count on Thursday September 02, 2021 @05:42PM (#28397739)
Formally verified programs often still have bugs. AWS S2N, for example, currently has hundreds of open issues and identified bugs, despite being the subject of a continuous formal verification program.

Bash powers probably hundreds of billions of dollars worth of critical infrastructure...

[ Parent | on HN ]
Re:I interviewed Brian J. Fox, the creator of Bash by pabs3 on Friday September 03, 2021 @12:17AM (#28400366)
There are attempts at formal analysis of shell scripts, for eg:

https://colis.irif.fr/ https://github.com/colis-anr/morbig

[ Parent | on HN ]
Re:I interviewed Brian J. Fox, the creator of Bash by nexuist on Friday September 03, 2021 @12:35PM (#28406391)
My point being that whatever other software runs on this thing is far more likely to contain hidden bugs than bash has given its age and widespread distribution. It seems weird to single out bash as opposed to the hundreds of other random packages on any given distro.
[ Parent | on HN ]
Re:I interviewed Brian J. Fox, the creator of Bash by varjag on Thursday September 02, 2021 @03:26PM (#28396254)
Ariane 5 bug was formally verified.
[ Parent | on HN ]
Re:I interviewed Brian J. Fox, the creator of Bash by sigzero on Thursday September 02, 2021 @04:45PM (#28397129)
No it really wasn't.
[ Parent | on HN ]