Hacker News Reader

Not even going to dependent types, the type system and verification capabilities of the SPARK language & toolset already allow for use in the mission-critical (and not only safety-critical) domain.

The tech is progressive so you can go first for 'correct' data flow (no access to uninitialized variables, dataflow constraints like Depends, Global, very interesting stuff already), then for proof of the absence of runtime errors, then for some specific properties (think maybe properties like 'this should never happen' or properties you'd write when doing PBT) to full functional proof. On a procedure to procedure base.

The progress that's been made with support of floating point is amazing. Things that were hard 3 years ago now get proved without help. Pointers are now supported via a rust-like mechanism.

NVidia seems to believe in the tech (well at least for Ada) for some of its new firmwares. I've seen pure algorithmic code fully proven with similar effort as it would have taken testing /AND/ you always find bugs... People that have written some SPARK then start thinking and designing for proof. Code gets simpler, design clearer, loops more evident, added contracts help understanding the interface and clear the mind while reading code (like early returns would have done before).

I don't work for AdaCore or Altran UK but I think they're amazing minds at work here.

Maybe some folks are experimenting with it, but I would be shocked if SPARK achieves market share of 1%. Or 0.1%.

I think it's a bootstrapping problem, similar to rust adoption. People are now getting enthusiastic about a language with lots of static guarantees and a difficult-to-please compiler, and I keep reading people almost jumping to formal proof/verification ('now that I made all this effort and I get all those static guarantees, why not go the extra static verification mile ?'.

I think the rust formal-methods community should look at what's already been done with Spark2014 (Ada) and Frama-C. A large part is an adaptation of the language for proof (adding /executable/ contracts, some quantifiers, loop variants/invariants, expression functions), and another big part of the work is in why3 and all the SMT tech behind, so can be re-used 'for free'.

Sure not even 0.1% market share today, and I'm not even sure Ada is above this. But it's there, it's already mature, progress is very fast, and it can be tried out for free without 'asking for a quote'. Same for Frama-C.

Sure it's a paradigm shift, but it's not an academic tool with an obscure UI and no retargetable skills.

Another thing that prevents dependently-typed languages from being the future is that there are alternative verification methods that have so far shown greater promise (and receive even more grants). I think the reason for this is that some hear of those languages because they're fans of programming languages in general and maybe know something about programming language theory, and dependent types represent this discipline in formal methods research. But if you look at formal methods research more generally (e.g. read the programs of the relevant conferences), you see that this direction of dependent type systems is relatively small, and most of the research effort is focused elsewhere.

I feel that some of the discussion about those languages is like an amateur runner who's thoroughly amazed by the results of an Olympic runner to the point of obsession, without knowing that they're in the seventh place. So dependently typed languages have had some achievement, but other techniques -- from CEGAR model checking to concolic testing -- have had better results, and that's why they're getting more attention in the formal methods space. The main challenge, which you alluded to, is one of scale. So far only very small programs have been verified using any semi-manual formal deductive proof methods (of which dependent type systems are one instance), and other methods have shown somewhat better scalability.

> other techniques -- from CEGAR model checking to concolic testing -- have had better results, and that's why they're getting more attention in the formal methods space.

These techniques are tailored towards efficiently finding refutations or counterexamples where a program fails correctness. They are very effective at what they do, but they're best used in combination with formal proof, or as a sort of glorified automated testing ('fuzzing').

First, model checking is a proof technique, albeit in the model theory of the logic rather than in the proof theory; that it can find refutations is a major strength, though. Second, engineers build systems, and they care about the correctness of their system. This is something that cannot possibly be proven because a system is a physical object, and at best, what you can get are probabilistic guarantees (e.g. the CPU only performs the commands it is given with some probability). So what engineers want (as opposed to mathematicians or computer scientists publishing an algorithm) is a technique that most cheaply brings their system to the required correctness probability. Whether this means proving the algorithm correct or finding as many bugs as possible is completely irrelevant. So far, automated techniques like the ones I mentioned do a better job at that, and that is why they're currently considered more promising.

> First, model checking is a proof technique

It is a proof technique if you're exhaustively checking a finite model, but the usual meaning of "model checking" is not restricted to that case. You may be right that just getting the "probability" of some software failing to meet its spec low enough could suffice for some use cases. Probably for "global", cross-cutting properties where formal proof might be expected to be difficult.

> but the usual meaning of "model checking" is not restricted to that case

It is. That's the definition of the term "model checking" ("model" means a satisfying assignment for a logic formula). Some model checkers (like CEGAR) also exhaustively check infinite-state specifications (although, obviously, not in every case; BTW, that model checkers are exhaustive, meaning sound, does not mean that they operate by brute-force -- they do not). You are, however, correct that sometimes we model check only a finite instance of a program/spec with infinite states, but in this case it is that restricted spec that is model-checked. That is one of the many ways in which model checking is more flexible than deductive proofs.

> just getting the "probability" of some software failing to meet its spec low enough could suffice for some use cases.

It would, does, and must suffice for all use cases, and besides, there is no other alternative.

> Probably for "global", cross-cutting properties where formal proof might be expected to be difficult.

No real system can be guaranteed to be correct. It is a physical impossibility. There is simply no such thing as a system that is "proven correct" in formal methods; the best you can hope for is an algorithm that is proven correct or a system that is correct with probability. Even exhaustive (i.e. sound) techniques like formal deductive proofs and model checking only guarantee the correctness of a system with probability. An algorithm that is proven to give the right answer is only a probabilistic guarantee that the system will (because the guarantee that the computer will execute the commands given to it correctly is only probabilistic).

Mathematicians and algorithm authors can prove theorems; engineers only need, and can only ever hope for, probabilities. This is why while there may be some overlap in the computer-assisted techniques offered to mathematicians and algorithms writers, the study of software verification is concerned with a different problem.

> The reason is simple: those languages don't support normal industry development practices, where you don't have time to spend 10x the time on verification as you do on development.

In practice, these languages have good support for gradual development so no, you don't have to spend 10x your dev time on verification. You can focus your verification effort on the lowest-hanging fruit, such as properties that only depend on local reasoning, as opposed to non-trivial interactions involving the program as a whole.

(One potential issue for this is that dependently-typed languages are total languages, so any code that's 'natively' written in the languages must be proven to terminate. But partiality and Turing-completeness can be reintroduced in a fairly trivial way by resorting to a 'Delay' or 'Partial' monad.)

That same argument was--and sometimes still is--made about the type system in Rust. As someone who has been building a network core recently where a small amount of dependent typing (more than I can pull off in C++, where the templating engine kind of hints in the right direction by letting you parameterize types over values) would go a long way, I personally feel like dependent typing could easily be added to existing languages, and the secret is to just make the fallback be to a runtime hard-enforced check (so it feels like something of a compiler optimization, though one where I would like to then be able to insist/check--even if only by using some external linting tool--that it is happening at compile time).

There’s also the problem where inferring the types is not decidable, so we either get slow tooling/builds or an onerous development cycle of specifying everything. The latter would be unbearable when you consider how weird and annoying things relate to one another in large, enterprisey systems.

> There’s also the problem where inferring the types is not decidable

That's a "problem" already when using some Haskell extensions. But it's only relevant in non-trivial scenarios where writing out types is not much of an extra burden.

There’s not much point in providing such guarantees for most application code but there is great benefit for OS and driver code, and some benefit to most library code.

Just take security. Ensuring all applications are using the latest, secure, version of a library is a hard problem and so we should do all that we can to ensure the code is correct. How valuable this exercises is depends on the size of the audience of the library