What if the 'mathematical specification of its functionality' is incorrect? How to prove the correctness of the mathematical specification faster than the underlying environment, code and dependencies change?
IMO, formal verification is never going to work. It's very clear that a lot of people are desperate to see it used in mainstream software development, but every innovation which proponents have seen as an opportunity to finally prove its utility has only served to further discredit it.
Now proponents are at a point that they literally have to convince us that people who aren't able to write correct code are somehow able to write correct mathematical specifications!
This is quite an extraordinary claim given that the mathematical specification is an order of magnitude longer and more complex than the code itself... And every experienced software engineer knows that mistakes grow proportionally to the size of the logic... Unfortunately, mathematical spec is logic; just like code, except it's more complex and thus more error-prone.
And don't even get me started on the fact that APIs, engines and languages change constantly from under you and thus the mathematical spec would get completely invalidated every week or so each time you did an update. Unfortunately, even in the best case scenario, reality is always going to change and invalidate our proofs faster than we can publish them. By the time you've proven the theory, its underlying assumptions already ceased to hold true.
Even in a far simpler hypothetical world with just one piece of software; the software's own execution could potentially change the reality which it relied on to prove its own correctness and would thus invalidate its own correctness merely by executing.
> How to prove the correctness of the mathematical specification?
You can show that your specifications satisfy well-accepted criteria like confidentiality and integrity. This is usually done as the final verification step. For example, AWS just did it for the Nitro hypervisor used by EC2: https://aws.amazon.com/blogs/compute/aws-nitro-isolation-eng....
I feel like the exact same line could be used to argue the opposite point against formal verification.
I'm not saying that proof is inherently bad. If it was free, then I agree it would be good, but my point is that it's not free. Proofs are expensive to produce, maintain, they lock-down flawed implementations, focus on correctness but disregard more important aspects like modularity (I.e. loose coupling, high cohesion). Also; formal proofs discourage change and they create false confidence about reliability because sometimes the bug is in the spec itself, especially as the spec gets more complicated.
I think modularity is a more useful property to aim for in terms of achieving the right degree of correctness over the life of the software, in a practical sense.
Formal proofs can work against modularity if the proof must be rewritten in order to achieve modularity as requirements change over time; which is the reality for most software.
That means when one goes out of whack, someone will notice. E.g. let's say the mathematical property is correct, but someone optimizes some behavior. Without tests or verification that could break production or worse: not break it, but break security without anybody noticing.
> people who aren't able to write correct code are somehow able to write correct mathematical specifications
This describes about one or two thirds of the Theoretical CS academic community (conservative estimate) /s
> This is quite an extraordinary claim given that the mathematical specification is an order of magnitude longer and more complex than the code itself
I find this hard to believe. The mathematical specification for "array a is sorted" is "forall n in Nat: 0 < n < len(a) -> a[n] >= a[n+1]". The average sorting algorithm is usually a tad longer than this.
> the mathematical spec would get completely invalidated every week or so each time you did an update
Well of course nobody serious advocates for formalizing/verifying code that is subject to that much churn (be it internal or external).
This is almost always the case.
It's one of the frustrating things about the software industry; because everything is much more complicated than the customer is able to comprehend, a software company can promise anything and the customer can't actually verify.
So any software company/project which actually took the time and effort to fully handle the enormous complexity, they can't sell themselves based on that fact because every other company (who didn't invest the effort) is also claiming it and the customer has no mechanism to verify the claims until some major rare event occurs.
And most of the effort is required precisely to handle those 1% of rare situations.
When it comes to software, it's almost never simple.
What people think of as simple is rarely so.
For example:
Requirement:
"Just copy a file from folder A to folder B."
Minimal translation:
"Implement the capability to copy any file, in any format and of any size from SharePoint, located at a configurable path, with appropriate authentication and access control checks, then stream it in chunks to a different, configurable path inside an S3 bucket, also with appropriate authentication and access controls in place. Ensure that any disruption in either service which may occur while the file is streaming can be recovered from at the point it failed instead of having to restart from the beginning. Ensure that the retry mechanism is built-in and that the retry window is configurable; if the file cannot be copied within the specific time window, then an error should be sent via email to a configured email address. Ensure that the entire transfer is encrypted in transit... If the file happens to be a folder, then you must copy across all of its contents recursively up to a certain configured MAX_DEPTH to avoid DoS and ensuring that the system does not get caught in an infinite loop due to symlinks pointing to a parent folder... In this case, send an email to the configured address... Etc... Etc..."
And the thing is; if you tell AI "Just copy a file from folder A to folder B." - It will not meet your 'basic' needs because even if it does a great job at filling the gaps in your requirements, it will still take shortcuts. In order for an AI to avoid taking shortcuts, it would have to make you fill out a questionnaire and make you sign up for and configure services; it would not be a pleasant user experience. The user experience cannot be pleasant, because the AI cannot read your mind and it cannot know your intent.
Here's a thing: my intent and requirements actually are:
"Just copy a file from folder A to folder B."
All that access control and authentication and symlink nonsense? That's a self-inflicted problem that exists only in enterprise, and shouldn't be assumed - much less created - for regular users.
If we think about public infrastructure in an adversarial way, the same way we think about software systems; we could say that it's full of critical zero-day vulnerabilities.
I implemented a library for rendezvous hashing with skeleton in order to get a similar performance as consistent hashing; it gets much more complicated and IMO loses some of the elegance once you add the skeleton. Most of the challenge is that the skeleton structure relies on a tree and so has to be rebalanced sometimes and this means that sometimes you have to move around more keys than ideal. The startegy you can use to perform the rebalancing can become very complicated.
Though the 'virtual nodes' in consistent hashing also add a lot of complexity there.
People with aphantasia probably overestimate how good it is.
I think I have good visualisation ability (based on spacial reasoning tests and ability to visualise complex software systems) but it's not like seeing something in real life; there is much less detail. Though on the plus side, I can manipulate the scene flexibly; I can zoom in, rotate, hover but a lot of detail is missing.
It's not blurry, it's more like what happens when you watch an AI-generated video of a four-legged animal walking and you didn't immediately notice that there was a fifth leg which popped out briefly before disappearing again... Or a bunch of mice are running around and one of the mice splits into two. It has a similar kind of quality where it's not constrained by the laws of physics and I only really see what I choose to focus on. What I'm not focusing on essentially disappears. I can zoom into some detail and it becomes clearer/more realistic but I sacrifice the big picture view. It's not uniformly vidid like something I see in real life.
Though I think the emotions I experience are the similar to reality (if it's a memory) so it feels like re-living the moment. The emotional and conceptual aspect is higher fidelity to me than the visual.
Overall though, my thinking style is very emotions-driven. I think I have a kind of synesthesia where every logical and visual concept in my mind is associated with a complex feeling.
But ironically, I don't usually act emotionally in my day to day. People I know would say I'm very rational but it's like my emotions themselves are rational if that makes sense. I feel complex emotions though not very strong ones.
Sometimes I take up the most obscure hobby imaginable and then somehow it comes up on HN months later.
I discovered a plant near where I live which has really strong, thin, long leaves and I started twisting them together and it makes strong, shiny green twine. I made a 3 meter long twine and then wove it into a tiny basket.
It works with only 2 strands and you can do it by yourself without any tools; just your fingers. Though I found some 3D printed plastic parts online which have a component which looks eerily similar to the one in the article.
The most unethical aspect IMO isn't what they're building but the taxpayer money which those big companies are getting. These are essentially handouts.
Taxes are not paid voluntarily but coerced out of citizens under the threat of force. So when they hand out such large contracts, the government is taking from all taxpayers by force and giving it selectively to a few chosen people who happen to own shares of those companies.
Many of those shareholders aren't even US citizens!
I'm surprised that founders still care about all that stuff. They already made tons of money, who cares. None of it means anything. Nothing is fair in this society.
They don't mind the system working unfairly in their favor; they only have an issue with it when it starts working against them. At that point, it's too late; you have no voice.
IMO, formal verification is never going to work. It's very clear that a lot of people are desperate to see it used in mainstream software development, but every innovation which proponents have seen as an opportunity to finally prove its utility has only served to further discredit it.
Now proponents are at a point that they literally have to convince us that people who aren't able to write correct code are somehow able to write correct mathematical specifications!
This is quite an extraordinary claim given that the mathematical specification is an order of magnitude longer and more complex than the code itself... And every experienced software engineer knows that mistakes grow proportionally to the size of the logic... Unfortunately, mathematical spec is logic; just like code, except it's more complex and thus more error-prone.
And don't even get me started on the fact that APIs, engines and languages change constantly from under you and thus the mathematical spec would get completely invalidated every week or so each time you did an update. Unfortunately, even in the best case scenario, reality is always going to change and invalidate our proofs faster than we can publish them. By the time you've proven the theory, its underlying assumptions already ceased to hold true.
Even in a far simpler hypothetical world with just one piece of software; the software's own execution could potentially change the reality which it relied on to prove its own correctness and would thus invalidate its own correctness merely by executing.
reply