3 ms·

You can make software a predictive profession, by adding an order of magnitude of cost to every software development effort. 10x. It's not that it can't be done

by devoply 10y ago

You can make software a predictive profession, by adding an order of magnitude of cost to every software development effort. 10x. It's not that it can't be done. It's the market is not suitable for that sort of development. It's a management problem, not a software engineer problem. There are a huge number of combinations of various statements that have to be iterated over meticulously. If you want to write tests for each and every one of these conditions, it's going to eat a ton of time to do just that and hence add tons of cost to your project. Developers use intuition when dealing with logic, and they make mistakes or don't understand all the possibilities that could occur... because the brain is limited like that. You can't make them not do that. You can just test for it after the fact and fix problems that are identified, that potentially adds huge cost if you are looking to make it fully predictable. Lots of testing happens in production systems. Especially in open source software. Or during implementation of some library. Those are identified and fixed when identified. To do that within a single effort will add huge cost to the projects.

nickpsecurity 10y ago
"You can make software a predictive profession, by adding an order of magnitude of cost to every software development effort. 10x. " This is a recurting myth. The field of high-assurance software delivers it on a regular basis in regulated markets. They built tools and reusable modules that drove costs down a lot. Still high cost vs throwing crap together. So, methods were invented far as the 80's to get most of those benefits on the chesp. Cleanroom methodology got very low defects with cost modifier ranging from cheaper to 20 or so percent more extra. That debugging & hard-to-change codd were greatly reduced offset upfront cost. LOCK secure kernel reported about 38% extra cost with full, formal verification & leak prevention. Altran/Praxis does it today for their clients with a mix of Z, Ada, and SPARK for claimed 50% premium. None of these are "10x" higher. Maxed out at 1.5x for most. Market can bear that. Only proven weakness of highly-assured development is time to market. Features do take longer to build if verified thoroughly. Medium-assurance like Cleanroom has some slowdown but acceptable. Less debugging and breakage by extensions offsets that, too.
- michaelt 10y ago
  This is a recurting myth. "Comprehensive formal verification of an OS microkernel" by Gerwin Klein et. al. (2014) [1] reports that it took 20 person-years to perform a comprehensive formal verification of the seL4 microkernel, which was designed, coded, documented and tested in 2.2 person years. Did they mess it up and take 19 person-years longer than they needed to? I don't know much about this stuff but I thought Klein's work was pretty state-of-the-art? Are there better ways of doing this stuff? [1] http://www.nicta.com.au/pub?doc=7371 http://www.nicta.com.au/pub?doc=7371
  - nickpsecurity 10y ago
    I already told you what it took in numerous projects plus one company's regular work to deliver low-defect software. Vastly lower than that. That means something is missing in either your data ir mine. Thing is, the NICTA papers clearly tell us why: 1. They were mathdmatically proving equivalence of spec, security policy, C code, and assembly. Latter two were state of the art methods requiring more time and brains. Not necessary in most projects to achieve low defects or 0-days. 2. The methods were new. When that happens in formal developmemt, most of the work goes into building tooling and even figuring out how to apply the methods to the class of problem. The seL4 and L4.Verified reports said exactly that predicting that reuse of that tooling would drop cost dramatically. It did drop to a quarter later with COGENT. LOCK, Cleanroom, Praxis, etc reused existing tools and methods where possible to avoid huge costs. 3. Cleanroom, Eiffel, Ada, or even Haskell all cost similar to regular development in commercial use despite knocking out many issues more easily. That they achieve low defects and cost should already establish my claim (strong QA is affordable) as baseline.

by devoply 10y ago

nickpsecurity 10y ago

"You can make software a predictive profession, by adding an order of magnitude of cost to every software development effort. 10x. " This is a recurting myth. The field of high-assurance software delivers it on a regular basis in regulated markets. They built tools and reusable modules that drove costs down a lot. Still high cost vs throwing crap together. So, methods were invented far as the 80's to get most of those benefits on the chesp. Cleanroom methodology got very low defects with cost modifier ranging from cheaper to 20 or so percent more extra. That debugging & hard-to-change codd were greatly reduced offset upfront cost. LOCK secure kernel reported about 38% extra cost with full, formal verification & leak prevention. Altran/Praxis does it today for their clients with a mix of Z, Ada, and SPARK for claimed 50% premium. None of these are "10x" higher. Maxed out at 1.5x for most. Market can bear that. Only proven weakness of highly-assured development is time to market. Features do take longer to build if verified thoroughly. Medium-assurance like Cleanroom has some slowdown but acceptable. Less debugging and breakage by extensions offsets that, too.

michaelt 10y ago
This is a recurting myth. "Comprehensive formal verification of an OS microkernel" by Gerwin Klein et. al. (2014) [1] reports that it took 20 person-years to perform a comprehensive formal verification of the seL4 microkernel, which was designed, coded, documented and tested in 2.2 person years. Did they mess it up and take 19 person-years longer than they needed to? I don't know much about this stuff but I thought Klein's work was pretty state-of-the-art? Are there better ways of doing this stuff? [1] http://www.nicta.com.au/pub?doc=7371 http://www.nicta.com.au/pub?doc=7371
- nickpsecurity 10y ago
  I already told you what it took in numerous projects plus one company's regular work to deliver low-defect software. Vastly lower than that. That means something is missing in either your data ir mine. Thing is, the NICTA papers clearly tell us why: 1. They were mathdmatically proving equivalence of spec, security policy, C code, and assembly. Latter two were state of the art methods requiring more time and brains. Not necessary in most projects to achieve low defects or 0-days. 2. The methods were new. When that happens in formal developmemt, most of the work goes into building tooling and even figuring out how to apply the methods to the class of problem. The seL4 and L4.Verified reports said exactly that predicting that reuse of that tooling would drop cost dramatically. It did drop to a quarter later with COGENT. LOCK, Cleanroom, Praxis, etc reused existing tools and methods where possible to avoid huge costs. 3. Cleanroom, Eiffel, Ada, or even Haskell all cost similar to regular development in commercial use despite knocking out many issues more easily. That they achieve low defects and cost should already establish my claim (strong QA is affordable) as baseline.