In most industries that need software made for them it's hard enough to get people to care about spending enough time on informal methods let alone formal ones. I simply don't think most of the industry has had the breathing room and respect for engineering for this pattern to develop.
I think its also about tolerance for failure. For software that must not fail or where reliability commands a premium you would be wise to invest in formal methods. Core systems at aws for example. For throwaway CRUD code its just easier to try iterations on the problem and call it a day. Its not about respect just RoI.
We do. It's called a type checker. Every "formally verified" system is going to be partially verified. e.g. you might prove your sort procedure sorts, but did you prove its complexity? Under a cost model for integer compares or a cost model for page fetches? Or both? Multi-layer cache page fetch costs? How well you verify just depends on how well you decide to model the problem.
Speaking for myself (and I bought Hillel's recently published Logic for Programmers): It's not clear to me which formal method I should use. I'm certain the answer is "there's a different best one for each situation", but I don't want to know one for each problem I'll face. I'd rather have a definitive answer to what is the second best for all situations, similar to how we can answer "python" to that question when the question is about general programming
This blog is actually very useful... There's also the flip side, possibly due to the expense (technically, intellectually, and emotionally), where "IT'S FORMALLY VERIFIED!!" has become some marketing code for "it's safe, secure, and PFAS free..." - just because something is formally verified, doesn't mean it's secure or fit for purpose. It usually just means it conforms to a given spec "and that's that..."
In most industries that need software made for them it's hard enough to get people to care about spending enough time on informal methods let alone formal ones. I simply don't think most of the industry has had the breathing room and respect for engineering for this pattern to develop.
I think its also about tolerance for failure. For software that must not fail or where reliability commands a premium you would be wise to invest in formal methods. Core systems at aws for example. For throwaway CRUD code its just easier to try iterations on the problem and call it a day. Its not about respect just RoI.
We do. It's called a type checker. Every "formally verified" system is going to be partially verified. e.g. you might prove your sort procedure sorts, but did you prove its complexity? Under a cost model for integer compares or a cost model for page fetches? Or both? Multi-layer cache page fetch costs? How well you verify just depends on how well you decide to model the problem.
Speaking for myself (and I bought Hillel's recently published Logic for Programmers): It's not clear to me which formal method I should use. I'm certain the answer is "there's a different best one for each situation", but I don't want to know one for each problem I'll face. I'd rather have a definitive answer to what is the second best for all situations, similar to how we can answer "python" to that question when the question is about general programming
> similar to how we can answer "python" to that question when the question is about general programming
An ironic claim in the context of formal methods.
I think it's the culture is software engineering.
In a good delivery app/social network it seems like a waste of time to use formal methods.
When designing software for aircraft, pacemakers, fintechs, cryptography and DeFi protocols there is a bit of value for formal methods.
The problem is the often people with the food app/social network culture are hired to build DeFi protocols.
Which explains why so much money is being stolen form DeFi protocols of late.
So why people don't use formal methods.
- 95% of the time, the stakes are low
- 5% of the time, the engineers don't understand the value of formal methods.
Leslie Lamport once joked that if software developers were architects, they would first build a skyscraper and then later draw the blue print.
This blog is actually very useful... There's also the flip side, possibly due to the expense (technically, intellectually, and emotionally), where "IT'S FORMALLY VERIFIED!!" has become some marketing code for "it's safe, secure, and PFAS free..." - just because something is formally verified, doesn't mean it's secure or fit for purpose. It usually just means it conforms to a given spec "and that's that..."
https://blog.janestreet.com/formal-methods-at-jane-street-in...
I thought this article from Jane Street makes a nice complimentary pairing.