5 ms·
If you want certain technology to be commercially successful, it needs to provide value. For the most part, most code are tolerated to be buggy, in exchange of
by tanilama 8y ago
If you want certain technology to be commercially successful, it needs to provide value.
For the most part, most code are tolerated to be buggy, in exchange of fast delivery. And for most internet applications, a single error has limited scope, so the damage is controlled. For those applications, former methods are not something that could help them succeed, they don't even write a lot of unit tests.
However, in different scenarios, like financial trading or consistency protocol building, where a single mistake will either cause you millions or resulting in nonrecoverable data loss that make customers lose confidence in your product, formal methods ARE indeed being used.
So it is simply a cost efficiency problem. For most disposable application project, it is not worth it, so they don't invest. If the code of interests is critical, and deserve every effort to get it right, then formal methods will be favored.
- pasta 8y agoI sometimes feel this also a language or tool problem. For example an integer. In most languages and tools this is a primitive. But most of the time we need a specific type of integer, for example a positive natural number. You can use a unsigned integer for this but that will include a zero wich we don't want. So maybe you can use a type/domain object for this in your code, but what about the database field or communication methods? It all can be done but with a lot of hussle. I think it would help if we had more primitives that would work in the complete stack. But then the question is: should ISO 639-2 also be a primitive?
- patates 8y agoAda has subtypes for such cases: https://en.wikibooks.org/wiki/Ada_Programming/Type_System#Constrained_subtype https://en.wikibooks.org/wiki/Ada_Programming/Type_System#Co...
- Uberphallus 8y agoAnd checks on compile time are quite insightful, Ada tends to know beforehand if you're gonna run out of bounds.
- chii 8y agoOr, don't split between primitives vs objects. I think it's a mistake to make thet distinction in many language's design.
- Retra 8y agoThe result of that will not be easy to use objects, but hard to use primitives.
- TheFattestNinja 8y agoCan you give me more examples of FM used in finance? I feel like they should be used, but in my limited experience with finance-related gigs I've been aghast at the lack of even basic testing put in place...
- danpalmer 8y agoFrom what I've seen, most finance development seems to be "work hard not smart" – throw a lot of developers with a wide range of skill, poor development workflows, and QA at a problem, and then back them up with shifting the liability to someone else. This mostly works, it just costs a fortune and results in moving very slowly.
- patates 8y agoIt depends on the stakes mainly, but also the experience of the stakeholders of a project. Both extremes (heavily tested, proven code vs "let's hope this works" code) are common but usually you're not allowed to speak about anything because of non-disclosure agreements and proven or not, all code is manually tested like crazy anyway. You commonly get insane overhead and just working code.
- bronsa 8y agoAt Imandra (https://www.imandra.ai/ https://www.imandra.ai/) we've been collaborating with a few big names in finance, from our website: "In 2017 Aesthetic Integration partnered with Goldman Sachs to help deliver the SIGMA X MTF Auction Book, a new orderbook venue implementing periodic auctions. Aesthetic Integration used Imandra, our own automated reasoning engine, to formally model the Goldman Sachs design of the SIGMA X MTF Auction Book, verify its key properties, and automate rigorous testing. Now that the venue is live, Imandra is being used to perform ongoing validations of trading operations."