Kevlin Henney in 6 impossible things talked about how Jon Bentley, in his Programming Pearls, chapter “Writing correct programs”, showed an example of formal verification by formally proving his implementation of a binary search. His proof was wrong, his implementation had an overflow bug.
Joe Armstrong in Systems that run forever, self-heal and scale talk about a consensus algorithm that had been implemented in Erlang and proved correct. After a while, they got a bug report. The proof was wrong.
In Ada, you can specify contracts and the compiler can prove the contract is enforced. But nothing prevents the programmer from writing wrong contracts in the first place.
Alexander Stepanov, in his book “From Mathematics to Generic Programming”, discusses an often forgotten, but crucial thing. A proof is a social activity, not an exact and mechanical activity. A proof is nothing more than trying to convince others that your algorithm is correct. But you and your peers could all be wrong.
“Being careful doesn’t scale” is true, but the reality is nothing really proves anything.
Availability of talent no doubt is a major factor in the decision-making process. That’s not an entirely external circumstance though. If Ada does deliver what it promises, then there would be plenty of Ada programmers around. The problem is it doesn’t as we learn from the Ariane 5 episode. The language’s reputation of being a “safe language” actually lead to the accident by providing a false sense of security, allowing the bug to sneak through.
I started my participation on this discussion more than two months ago with that sentence. Yet here we are. This is the reason why I, personally, end up stepping back from this topic – I feel it quickly becomes straw-manned.
I disagree with the outlook of “everything, always, could be life-threatening” – I am not even going to go there.
I started by saying that I love having these errors. I really do, that was no exaggeration. After all, one of the reasons I throw my fortune with Zig’s lot is because it provides compile-time checking of many thing (types, obviously). But I also crave for flexibility: being able to just move forward while I am experimenting with my code. To make the point clear: I wouldn’t mind having a “relaxed” mode where no types are checked, and Zig becomes closer to a purely interpreted language. I am not even sure such a thing is possible; probably it is going too far; it might be useless; and yet, I would still play with it.
Also, just to be totally clear: I will keep using Zig, with or without this “sloppy mode”. The language is too good, too close to my ideal, for me to throw it away. I am perfectly happy accepting Andrew’s decision here; he has proven to have an unerring hand as the language steward. We don’t have to agree on everything to work together on something. Let’s not beat / manipulate each other into submission.
Peace.
Here is a link to a discord topic about a similar idea as a separate project: Zig Discord > requests > ZigScript it links to this gist ZigScript · GitHub and GitHub - marler8997/zigscript
But if you are really interested make sure to read the discord, there is more discussion there.
Yes and you have pointed out your opinion and I understand it, however people will talk about what they want to talk about.
I think all sides had plenty of time to discuss a lot of different aspects and personally I also feel like this topic has gone on long enough.
That is why I am voting to close this topic and to open new topics when somebody wants to discuss related things, or has actionable steps towards improving the situation, that weren’t already discussed over and over again.
- close this topic
- leave it open
*Edit accidentially created the poll with showing votes, I think this should be an anonymous vote.