Correctness – A paradigm for sustainable software development

No, I'm saying that there is no way to encode even such a simple property as 'addition of two numbers produces a bigger number' in the type systems of most languages out there (including stuff like the ML family), which is probably why (non-dpendent/linear/other advanced) type systems have never been shown to improve program correctness the way other formal techniques have. Even simple type systems help in other ways (ease of development, documentation, performance).

If you force your types to only ever interact with primitives at certain boundaries of your app, you can test for the "what if it's not an integer" stuff at the boundaries only. I.e. the core APIs never see a magic string, an integer, or any other such untyped thing.

In reality, there are always times where that falls a little flat, which is where IMO Gradual Typing comes into its own. The "core", with some assumptions about the boundaries, be statically analysed. You can add your times(int n) method safe in the knowledge that you'll get a runtime error if someone messes up the dynamic type or doesn't run the analyser.

Ultimately, as I want to run all my code before I put into to production, a lack of runtime errors from my tests tells me my code is correct for the situations I designed it to handle. Now if someone comes along later and manages to invoke a state that I hadn't considered, well... all bets are off.

Absolutely, but first, CompCert is not really a good example for verification. It is a very small program (roughly equivalent to 10KLOC of C; i.e. 1/5th the size of jQuery), it has taken years of effort by world experts, and they had to cut quite a few corners so your classification of what exactly has been proven is also exaggerated (watch talks by Xavier Leroy [1]). It is more a heroic story of people who climbed the Everest naked than some generalizable technique. But heroic and impressive it was.

Now, CompCert was verified using deductive proofs. In industry, this is an approach that's hardly used (in part, CompCert was done to show that it could be used at all, at least in principle). Verification in industry is normally done using model checkers, that are fully automated. There are tradeoffs between deductive proofs and model checkers (and sometimes deductive proofs are used to close some holes left by model checkers, or tie together some modules verified by model chekcers [2]), but they scale better. Model checkers used in industry include Spin[3], nuSMV[4] and others.

So model checkers check software that's larger than CompCert every day, but they don't get papers written about them, because their use is more mundane than heroic. They are also used for imperative languages, because formal verification of functional programs is behind (here is Simon Peyton Jones saying that [5]). Model checking functional languages is hard, because higher-order functions are hard to verify. Instead, there are model checkers for C, Java, hardware definition languages and tool-specific languages.

So, this mentions a 1MLOC Java application by Fujitsu that's been model checked[6] with NASA's Java model checker (that's 10x bigger than CompCert), and here's a report about model checking a many small C programs[7]. Again, software verification of imperative languages is almost mundane; what you read about are exceptional things.

Also, people who are interested in programming languages are normally introduced to formal methods through its small intersection with programming language theory, and that intersection includes uses of proof assistants and dependent types. Because functional languages are liked by language theorists (for many reasons I won't go into), then that's what you see. But that is a very small part of formal methods research. Most of it is research into model checking and sound static analysis, and most of that work is done in imperative languages. Not because they're easier to verify (both functional and imperative are just as hard, but pose different challenges), but because they want to check programs in languages many people use, and language doesn't make much of a difference.

Finally, I should add that even though language doesn't have a huge impact (there can be some exceptions; e.g. unsafe languages such as C do add some challenges), there are languages that are more natural for verification; they are not functional or classically imperative, though, as those two are both mediocre. Rather, those languages are synchronous languages (usually imperative, but not like what you're used to). Normally, those languages are used in hardware and real-time software (Esterel[8], SCADE[9], but they are now starting to make their way into the mainstream with Céu[10], "behavioral programming" in JavaScript [11], and, perhaps most famously, with Eve [12] (RIP). To see why these synchronous (but imperative) languages are a good fit for verification, take a look at how easy it is to specify a correctness property in Eve: [13].

Finally, my own favorite specification and verification language is TLA+ [14], which is neither functional nor imperative (but it is synchronous; then again, it's not a programming language), has been used to verify very large programs at Amazon and elsewhere [15].

To get back to where I started, CompCert (and seL4) are not really examples of anything. They were both huge, heroic efforts (that didn't quite prove as much as you think they did) by academics in the lab on quite tiny programs. While these efforts are important for some niches, you can't generalize, just as you can't generalize from the design of particle accelerators used to turn some lead atoms into gold atoms to learn about how best to design metalworking tools. Full, end-to-end verification, is something that we simply aren't yet capable of doing in any generalizable or scalable way, regardless of language.

Real-world verification efforts are quite different, and are done with imperative languages both because that's what people use and the language doesn't have a big impact, and becuase there are still issues with model checking functional programming languages.

[1]: http://video.upmc.fr/differe.php?collec=S_C_colloquium_lip6_...

[2]: http://events.inf.ed.ac.uk/Milner2012/J_Harrison-html5-mp4.h...

[3]: http://spinroot.com/spin/whatispin.html

[4]: http://nusmv.fbk.eu/

[5]: http://events.inf.ed.ac.uk/Milner2012/Monday_Panel-html5-mp4...

[6]: http://javapathfinder.sourceforge.net/events/JPF-workshop-05...

[7]: http://www.csl.sri.com/users/ddean/papers/ndss04.pdf

[8]: https://en.wikipedia.org/wiki/Esterel

[9]: http://www.esterel-technologies.com/products/scade-suite/

[10]: http://ceu-lang.org/

[11]: https://youtu.be/PW8VdWA0UcA , https://vimeo.com/298554103

[12]: http://witheve.com/

[13]: http://witheve.com/#correct

[14]: https://lamport.azurewebsites.net/tla/tla.html

[15]: https://lamport.azurewebsites.net/tla/industrial-use.html

> Namely, is crappy software actually more efficient?

I have many many examples from real life, for instance, one from banking; sometimes I have to work with systems that are responsible for 100s of millions of $ in transactions that are just ductaped heaps of crap. They are running on many servers because they continuesly crash and mess things up (literally corrupt data which has to be manually fixed).

The software was written by juniors with a lead tech who only made some web scripts before and all was hurried to the 'finish line' to get more investment.

All of these decision where economic; hire cheap people to show bums on seats, hire cheap management because good management costs a lot keep pushing for deployments even though everything is ill tested because the need for more money.

The result is that the entire team is all day (and night) busy putting out random appearing fires and the average period for an employee to stay is 6 months after which the stress catches up.

Ofcourse they still are doing really well as these type of companies are experts at hiding things like this. Thick rows of sales and account management people to hide the poor execution. Reminds me of IBM in the 80-90s; slick looking suits and shiny boxes but the software they shipped was just pure vomit; it still sold fine (not sure if it changed; I have not worked with them anymore).

Obviously they would be really raking it in if there weren't 40 people 24/7 trying to keep the stuff on the servers from completely exploding.

After a week of hard work in these kind of circumstances, I always enjoy reading HN + Reddit in the weekend and seeing these wide eyed youngsters here thinking that every company does code reviews, unit tests, uses versioning tools (...), not using php for near real time banking backend banking transaction applications (...), kubernetes/docker, microservices, serverless software while in reality it is a microscopic % and very large numbers of money is still being earned through absolute software poop.

Polymorphic modules are a necessity for system design. To be used sparingly. Turns out that Java/C++/C# provide a mechanism for polymorphic modules at language level.

Beyond that, failures all around. On top of my head:

* The insistence of designing systems fragmented in tiny state machines instead of systems processing immutable values passed around wholly and processed by pure functions. In the UI domain we finally got back to our senses with React.

* The insistence that values do not exist, but rather objects = data + code. Leading to brittle abominations like CORBA, agents, etc. For distributed systems, a humble RPC passing values [NOT objects] back and forth is infinitely more valuable.

* The insistence that inheritance is a useful design mechanism, leading to highly coupled codebases. Also, a prime cause for object-relational impedance mismatch.

* The insistence that one should overengineer code for extension without modification at every turn. How about just write the simplest version of the code for today, and refactor it if new requirements pop up.

* The insistence on messaging as fire-and-forget [aka goto] instead of structured function calls. Decades after we've learned why goto-oriented programming is a poor idea.

* The insistence on overusing polymorphism to mock everything in testing. Making it hard to trace how the codebase actually operates, and making it expensive to change the codebase because tests and code are tightly coupled.

* The insistence on overusing polymorphism for all type-based dispatch. Try writing a compiler in a purist OOP style, with a visitor for every type-based switch. Maybe it works in Smalltalk, 'cause in Java/C++/C# it gets boilerplaty really fast. Or even better, "encapsulate" your AST data into "objects hiding their internals" and do all type-based dispatch using vanilla polymorphism. Nothing screams "fun" like wading through tens of files to piece together what should have been a single switch block.