Coming Soon: Machine-Checked Proofs in Everyday Development
media.ccc.de
media.ccc.de
- Fundamental Proof Methods in Computer Science
- Handbook of Practical Logic and Automated Reasoning
- Software Abstractions
- The Little Prover
Yes, currently I have Athena, OCaml, Alloy, ACL2 (via Dr Racket/Dracula) all up and running to work through the exercises in these books. I'm very skeptical anything will come of this, but it interests me and I can see the value.
Hopefully the speaker's next book Formal Reasoning About Programs (https://github.com/achlipala/frap) will be a nice next step, I have Certified Programming with Dependent Types but have not cracked it yet. Also keeping an eye on Verified Functional Algorithms (https://softwarefoundations.cis.upenn.edu/vfa-current/index....).
Do you mean The Little Prover?
Even unit tests which don't involve proofs can be a problem sometimes because they lock down API inputs and outputs. It's already a major problem when a developer wants to change some code and they have to spend hours updating unit tests every time. When in small teams, heavy 100% coverage unit tests slow down productivity, possibly by 5x or 10x.
I imagine that adding proofs as part of the unit test suite would further increase the productivity cost overhead by a massive factor.
In software development, you should avoid treating the code like if it's special or perfect because it's not and it will need to be changed in the near future when requirements change (and they will always keep changing). So locking it down into a specific state with proofs all around it is a bad idea for the vast, vast majority of cases.
We need more wisdom in software development and that means taking a step back, looking at the big picture and asking questions like what are the negative side effects of each new methodology that we are introducing into our projects? There are always downsides, and we're crazy to pretend that every fancy new methodology is a silver bullet.
My unit tests are basically "comments" for my code, that show me how the code is supposed to work. When I make changes, the tests will tell me if I broke the intentions of the initial developer.
Sure, when doing big changes, just updating and maintaining the tests is a lot of work, but so would maintaining documentation and comments be. So we have less documentation and fewer comments, and more tests.
If the code itself is written properly then the individual classes and objects used throughout should be high cohesion and easy to read without needing any comments or tests.
There are always cases where unit tests are important though like the parts of the code that deal with money.
But there is no benefit in adding unit tests if you're building a standard chat system for example; integration tests are sufficient in that case.
Also getting 100% test coverage is a complete waste of time if you don't actually test the right kinds of input and output parameters.
Had a lot of "fun" rewriting a bunch of integration tests for angular, because the framework used a lot of Promises which caused race conditions. Those tests were much harder to write than unit tests and were much easier to mess up.
Stubs are not just useful for unit tests. Service stubs are often much easier to write than module stubs because services often communicate via string based protocols which are easy to simulate.
In my experience brittleness in tests is caused by bugs in tests or bugs in code.
Most of these things can be fixed, e.g.
* Add an order by to select statements that otherwise returns data in an indeterminate order.
* Fix the interpreter/database version you are using to run your code rather than relying upon the version the package manager has installed.
* Stub out code that gets date/time/random numbers.
* Stubbing out external APIs which go down on Tuesdays.
* Fixing the bugs in your code.
* Abandoning the code you rely upon which is buggy (I'm just sayin', angular might not be the ideal framework).
Avoiding writing these tests because you know that "they'll be too buggy" doesn't exactly send out a great signal.
>Such tests are great for detecting that something is wrong, but it can be very hard to figure out what's wrong and where things went wrong.
This is alleviated by integrating debugging tools into your test environments.
"100% test coverage" usually means statement coverage due to the nature of popular tooling.
If you deeply care about correctness you are usually more interested in path coverage which is more tied to things like heap shape or state space... (which depending on your system design might encompass stuff in your database). Also yeah, technically the exceptions which can be thrown at each point in your software if you work in a language with those.
Unfortunately there's not much tooling for that so it's not visible in the same way as the more naive metrics.
Anway my point is that you can waste time pushing for "100% statement coverage" measurable by naive tools but still not exercise important paths, which I think is your point.
Disagree. Finding the right amount of unit testing is an optimization problem. Some amount is nearly always useful.
For starters: Integration tests will not necessarily exercise a full range of inputs for the low-level functions. For a chat system, I would think hard about how to test low-level functions with a wide range of Unicode input.
A chat system must survive in the harsh environment of the public internet. It needs to be hardened against unexpected user input, either incidental or malicious.
I don't see any problem at all with writing integration tests that exercise a chat system with a wide range of unicode input.
I'd view it as irresponsible not to, in fact.
The most reliable way to address this kind of problem is to match the tests to the function. Look at what each function does, anticipate edge cases, contemplate the core purpose, then write what you believe are an appropriate number of unit tests.
You can choose not to prioritize the problems which are revealed by unit testing but not integration testing, but you can't say that such problems don't exist.
Um, disconnection from the service is the exact kind of scenario I'd want to repeat exhaustively in an integration test.
Well, that's asking me to disprove a negative. All I can say is that I don't think that principle is true.
One counter-example of a scenario that is impossible to integration test but possible to unit test would be sufficient to disprove my hypothesis, but I don't think it exists and I don't think you can provide it.
>Even if you take every example I give and claim "doesn't count, I'd test for that", you're just writing unit-tests-once-removed using an integration testing framework.
I'm really not. I can test disconnection scenarios in an integration test without even coupling to the language under test by running a service that intercepts network traffic. It's obviously not a "unit test once removed" if I can literally swap out the entire language under test and not have to change the test.
I mostly develop backends of web apps. In my experience not every web app has some code that needs to be explained. Picking the correct names is usually enough.
That said, unit tests really do what you write: provide examples, use cases and guidance.
So there is a possibility that changing the code only forces you to change theorem statements (that is, the spec), allowing reuse of the proof script itself. Now you are doing software engineering on proof scripts, and you face the same generality/flexibility problems you would face when writing unit tests. A well-written proof script would be flexible enough, and a hacky one would lock things down too much.
There cannot be a program that can prove (or even help a human to prove) any true statement about programs written in a Turing-complete language.
Generally don't test against internals much, except if an area is shown to be buggy and hard to exercise externally.
Prefer (well tested) libraries for generic functions/algorithms. If you have to implement one, put tests on it as if it was external API. Consider publishing it independently to make it external. If needs change, just drop the dependency.
It depends what kind of math and what they're doing though. Systems like Coq give you much more trustable code to put in your system, and higher degrees of trust for clients. But systems like Idris actually let you write code and use the proof engine to write trustworthy code.
Most of that "math", from the perspective of a programmer, is a small subset of graph theory, formal logic, and category theory useful for proving relationships and reflexivity so that the machine can help you.
> Even unit tests which don't involve proofs can be a problem sometimes because they lock down API inputs and outputs.
This is a much bigger problem than "hand written mocks are bad" (which they are, I agree). But it's quite out of scope to complain that because API endpoints are often sloppily deployed without versioning or introspectability, that all formal methods are wrong.
What's more, and I really want to push this point so I'll emphasize it: quickly producing broken code helps almost no one. If you're an artist playing with making a synthesizer whine? Maybe okay. If you're writing software intended to face the world and do real work? We can't just keep pretending we're all smart enough to do this without mechanical aid; we're NOT smart enough to do this without mechanical aid anymore. Programs integrate too many libraries and APIs.
> I imagine that adding proofs as part of the unit test suite would further increase the productivity cost overhead by a massive factor.
With Idris, it makes it so the program can write code for you. I've been learning it over the last 2 weeks and I'm totally fascinated by how much drudgery it takes out of total programming.
> In software development, you should avoid treating the code like if it's special or perfect
This is precisely what formal methods do! You challenge every piece of code you can and say, "Prove to me that what you've written doesn't have an obvious flaw!" You rewrite until both the human and the proof engine cannot see anymore. It is not sacred at that point (no one believes this), but at least you've acknowledged that you can write errors and started to mitigate them.
> There are always downsides, and we're crazy to pretend that every fancy new methodology is a silver bullet.
Actually, the entire industry has started to demand that developers do a lot more computation on their ends to make better software. The "prove more of your program and write total code" is just one side of the "do more work on your end" school. Another is, "Your software is in fact the output of this algorithm training from a dataset on 4 GPUs." We probably need a similar step forward for APIs (where APIs are invalid & unusable without a spec that governs them).
It is a change, but most commercial software engineers are handling user data that can be leveraged in disastrous every day. As you say, we need the wisdom to realize that it's difficult to guess the use case or security impact of the code we write on a daily basis, and we need to start taking that fact seriously. These heady days of being able to deny responsibility and shove out any software we want without consequence need to end.
It's not so much that they're "all wrong", but when the majority of bugs you face are not logical or algorithmic in nature but driven by incorrect specifications or problems dealing with the outside world (including but not limited to sloppy APIs), then formal methods will impose a stupidly high cost for almost no benefit.
To take the famous Mars Climate Orbiter bug as an example - had the software been formally proven then it still would have gone down in a ball of fire because the software was built upon a faulty presumption. An integration test that exercised both the data and the code in a realistic environment would have saved it though, as would better spec communication between the two teams (e.g. some form of BDD). The chief investigator, Arthur Stephenson, even explicitly called out the lack of sufficient end to end testing.
I'm sure formal methods are great for proving that, e.g. a particular sorting algorithm always works, but frankly, sorting algos are the type of thing I import and just assume works and I've yet to see a bug in the wild that invalidates that assumption, whereas a faulty interaction between two poorly specified modules is a problem I see in teams on a near daily basis.
But automation could verify this. Unit tests don't do anything if they aren't run. Specifications don't do anything if they aren't checked. Do you have CI/CD? Use it!
> then formal methods will impose a stupidly high cost for almost no benefit.
Except that lots of business logic errors, resource handling errors, and mathematical errors still exist in modern code at all levels. And you're also assuming the "cost" is "stupidly high" which people in this thread are telling you is false.
Finally, please forgive me for being so blunt... If you're delivering code you haven't tested to hit a timetable, you're part of a scam. People don't want broken code. People aren't buying security holes. People aren't asking for things that almost work but then dump user data by the score. No one wants this, but developers like us keep insisting it's fine because they're not personally responsible.
I wish that you or I could be fined if we didn't show due diligence. It'd be good for the industry.
> To take the famous Mars Climate Orbiter bug as an example - had the two individual modules of software been formally proven then it still would have gone down in a ball of fire. An integration test that exercised both modules would have saved it though, as would better spec communication between the two teams (dare I say it? BDD).
> To take the famous Mars Climate Orbiter bug as an example - had the two individual modules of software been formally proven then it still would have gone down in a ball of fire.
Cool, except that the module integrating these, if validated, would have caught this. Which brings me to my second point:
> An integration test that exercised both modules would have saved it though,
I'm not sure why you think using a computer to write proofs about your software somehow magically excludes integration tests. Excluding integration testing is something humans already do well.
If anything, running a type checker and using pre-existing proofs on an new module that integrates them is much more than most people do.
> as would better spec communication between the two teams (dare I say it? BDD).
The irony here: BDD is a less formal but similar technique to writing proofs. BDD could be integrated directly into the development piepline (as it is with Idris) and the compiler could tell you when you missed a spot, or forgot to handle something.
It seems you only dislike it when the compiler does it.
> I'm sure formal methods are great for proving that, e.g. a particular sorting algorithm always works, but frankly, sorting algos are the type of thing I import and just assume works
What is the difference between checking if a program properly closes a socket or if a sorting algorithm works? From a proof checker's perspective: it's very little.
> sorting algos are the type of thing I import and just assume works
And this is and example of the mentality that ensures that despite the fact that we've seen the O(n log n) speed limit for sorting shattered, no one knows or cares.
> whereas a faulty interaction between two poorly specified modules is a problem I see in teams on a near daily basis.
Why don't you want to make it easier to write better modules, and make it easier to verify the integration of modules? "It's hard so I won't even try," seems to be your reasoning here despite several people saying it's possible.
Yes, that's what I was arguing.
>Except that lots of business logic errors, resource handling errors, and mathematical errors still exist in modern code at all levels. And you're also assuming the "cost" is "stupidly high" which people in this thread are telling you is false.
My experience with formal proofs is it imposes a high cost. I don't think that there are people in this thread who believe that you can impose formal proofs on a system without incurring a significant cognitive overhead (and possibly other costs too). If they exist, they are simply wrong.
>I'm not sure why you think using a computer to write proofs about your software somehow magically excludes integration tests.
I'm not saying that it does. I'm saying that the kinds of bugs unveiled by formal methods are, in most applications, rare and obscure and the bugs unveiled by integration tests are, in most applications, common and important.
When I have limited resources (everybody has limited resources), I tend to take the approach that has the best ROI in finding bugs. For most applications, that isn't formal proofs.
>Cool, except that the module integrating these, if validated, would have caught this.
You still aren't getting it. The module was built upon faulty presumptions. Peter Norvig himself said that no language, no matter how type strict, would have enforced this convention.
>The irony here: BDD is a less formal but similar technique to writing proofs.
I'm sorry, but writing user stories on the back of a napkin (yes, that's BDD too) isn't a similar technique to formal proofs in any way, shape or form.
BDD is simply a means of communicating example driven specs that may or may not be turned into executable user stories.
Automated tests (a common side effect of BDD) are not really similar to proofs either.
>What is the difference between checking if a program properly closes a socket or if a sorting algorithm works?
The likelihood of bugs in the definition are significantly higher the less abstract your code gets. To wit: maybe your presumption that the socket needs to be closed is wrong.
>Why don't you want to make it easier to write better modules, and make it easier to verify the integration of modules?
I absolutely do, that's why I use the right tool for the job.
What is that experience within the last 5 years. Does it include Idris, Agda, and Coq?
> I don't think that there are people in this thread who believe that you can impose formal proofs on a system without incurring a significant cognitive overhead
The idea is that by asking humans to make small proofs, the remainder of the majority of additional cognitive overhead can be assumed by the machine.
This conversation has a curious pre-assumption that this cognitive load is "new". In fact, it's not. It's an alternative approach to working with the complexity already apparent in our domain.
> You still aren't getting it. The module was built upon faulty presumptions. Peter Norvig himself said that no language, no matter how type strict, would have enforced this convention.
Why is Peter's comment relevant here?
> I'm sorry, but writing user stories on the back of a napkin (yes, that's BDD too) isn't a similar technique to formal proofs in any way, shape or form.
It is if you care about the results. A lot of modern BDD process has humans as verifiers. And no one's saying that has to go away. But we might need it LESS for certain parts of the system.
Certainly in my user-facing fintech applications I have wished for tools that could do this. Sadly a lot of my work in that field predates the usability of a lot of these tools.
> I absolutely do, that's why I use the right tool for the job.
And the right tool for the job is evidently not a computer?
What I think you're missing is that these formal proof systems come with an implicit power: the ability to extend the a more generic type system at build time to reason about your domain.
This application is as radical in nature as it is classical. Everyone in every domain has suggested for half a century that we work to bring our code closer to our domain and further from the minutiae of machine implementation. Modern systems seek to do this by creating stable abstractions to build upon.
This takes 2 shapes: trained by data (classifiers, regressions, and statistical methods) or refined by logic (proofs, dependent types, type inference and verification). The line between these types is somewhat transient, and over time it's almost certain it will blur. Already we see F# using "Type Providers" that let you use samples derived directly from an API (or specs, or both). These can be obtained as part of the build process, and then the program can be checked against the spec.
There is only one real downside to this approach: it makes development require even more computational power. But given that we're solving a much harder problem than the users of our software, the asymmetry seems reasonable.
I think you and I agree in the general strokes but you don't like the word "proof", if I'm being honest. I don't know why that word bothers you so much. Did you watch the video? Have you tried Agda, Coq and Idris?
Right now the benefits of static verifiers is rather binary. Either your program (or code unit) is sucessfully verified or it isn't. And every time you make a change to verified code you risk losing its verified status.
Imagine instead writing code that is made "safe" using run-time asserts everywhere. Unoptimized, this code might be slow. And unreliable in the sense that a run-time assert could fail, requiring some kind of recovery or abort action. But it would still be "safe".
The run-time asserts are effectively the "program specifications", and the discarding of those asserts at the optimization stage is basically equivalent to traditional static verification. The difference being that not quite fully optimized "safe" code is generally more valuable than not quite fully verified (and therefore not fully "safe") code.
> These heady days of being able to deny responsibility and shove out any software we want without consequence need to end.
If the static verification community is imploring the development community to, with some effort, change its practices to improve code safety, would that community be willing to, with some effort, move the application of their verification logic to the optimization stage where it would be more practical for a wider range of applications?
They can be applied at lots of stages. Why not apply them to all of them?
> Either your program (or code unit) is sucessfully verified or it isn't.
This is demonstrably false. It can help you write better, safer code incrementally. Every approach that is discussed here has a "refinement" plan.
> Imagine instead writing code that is made "safe" using run-time asserts everywhere.
I can imagine this, it's the C/C++ style of code circa 2010. It's awful for users. But it's not what we're discussing here.
> If the static verification community is imploring the development community to, with some effort, change its practices to improve code safety, would that community be willing to, with some effort, move the application of their verification logic to the optimization stage where it would be more practical for a wider range of applications?
Yes. You're already seeing two major examples of this: Type Providers and derivations of dependent types fall into one camp, dependent type implementations (of which the most prominent is Idris) fall into the other. All of them offer the ability to extend the type system and make proofs useful to developers even as they also help make code total and enforcible.
I think it's further along than you seem to suggest. Can I suggest you grab a copy of Atom, Atom-Idris, and go through some Idris tutorials? You can also try F# and use Json samples pulled from an API to generate types that inform your tooling and improve code quality.
We're starting to see a change in the economics. There's quite a way to go -- I hope we get there intelligently and not as some kind of thrashing reaction to giant disasters.
Yes, real money in smart contracts is part of the economics shift I brought up.
We have a lot of experience building programs that help us program (e.g. compilers, IDEs, build systems) We can move forward without falling into traps (low performance, high programmer knowledge required, overly rigid, more work required than gained in productivity)
There are no silver bullets but we can continue to improve.
A bit of self promotion, I touched on this in a recent blog post if you're interested in this sort of stuff: https://performancejs.com/post/hde6a33/JavaScript-in-2017:-Y...
The future is here, but not evenly distributed. ;)
Would the resources in the original post be worth looking into to build secure contracts?
How would such a proof checker know the intent of the code of not having backdoor/insecurity? How do you define security in a logical sense?
As you surely know, there is no such thing as secure/insecure, but a set of properties that are considered in IT security, which might even not be fullfillable all at the same time. The exact words vary depending on the book, but a popular classification in a German standard reference on IT Security is
General protection goals:
- Integrity
- Confidentiality
- Availability
Further goals are
- Authenticity
- Acountability
- Non Repudiation
- Sometimes Anonymity
So you first begin to formulate your protection goals. Next you can begin to forumulate this in a logical sense. Again there can exist quite different axiomatic implementations of a general protection goal.
But since you want to see examples:
A common model in literature for integrity is the Biba model: https://en.wikipedia.org/wiki/Biba_Model
Another common model for integrity is the Clark-Wilson model: https://en.wikipedia.org/wiki/Clark%E2%80%93Wilson_model
The mathematical dual of the Biba Model is the Bell–LaPadula Model for ensuring confidentiality: https://en.wikipedia.org/wiki/Bell%E2%80%93LaPadula_model
A model that ensures that the access rules will be free of conflict of interest (this of cause involves privacy and integrity aspects) is the Chinese Wall Model: https://www.cs.purdue.edu/homes/ninghui/readings/AccessContr...
This makes the clarify of specifications into a market-driven problem. What do you do if you have a formally proven contract, but nobody can understand what the spec is? Well, you probably won't be able to sell it, because nobody will trust you. Instead, you try to simplify the specification, so you have something that people will trust. This is very similar to established practice of mathematics, where getting a proof accepted is really a social process, in which you try to convince your fellow mathematicians that the proof is correct.
https://www.cs.cornell.edu/andru/papers/jsac/sm-jsac03.pdf
https://www.cs.cornell.edu/Projects/fabric/
The concept was taken to the binary with Necula's Proof-Carrying Code. Work like Kumar's and Davis' eliminated most of the TCB of the provers, too.
https://www.utdallas.edu/~hamlen/Papers/necula97proofcarryin...
http://www.cse.chalmers.se/~myreen/runtimes.html
In parallel, there's always work in capability-based security applied to programs or OS's. Here's an old and new one using that model.
I wrote up what this could look like: https://pastebin.com/raw/ZAys0mYp
It's worth noting that Ethereum's "fuel" model as a 1:1 correspondence with how Idris's mostly-total IO monad works. The "infinite fuel" bit can just be turned off and some (substantial and tricky, I admit) changes written to keep top-level state around and bam; timeboxed resume-able IO
That's where I thought we were in 1983 - ten years away.
> That's where I thought we were in 1983 - ten years away.
Obligatory xkcd:
God I cringe every time someone posts that. It's like the "Big Bang Theory" of internet comics.
The problem, it turns out that they included a new version of OCaml which was incompatible with the older version of GTK that was being used. Result: crash due to seg fault.
We really need both proofs and pragmatics. Proofs can give us confidence in the fundamentals when used appropriately for the processor, or for consensus algorithms like Raft, or key parts of the OS. Tests and statistical analysis can give us confidence that we haven't overlooked something crucial.
Some systems obviously aren't very appropriate for formal methods (take machine learning, for instance, there can be no formal spec for what a fraud looks like). There statistics and testing will have to suffice because we have clear value on average even if we cannot formally guarantee the system.
Other systems are much more appropriate for formal methods. I should hope that a heart monitor, CPU, voting machine or aircraft flight management system will have substantial amounts of formally proved code (I know that I am dreaming with the voting machines; let's settle for getting it down on paper). I don't want to collect a statistical sampling of whether an airplane works as we iteratively work out the bugs and specs in an agile fashion.
So, one question: Adam gives one example of a proof where the initial automation fails because it does not consider a theorem that was previously proved. He also gives an example of some complex code where the proof is too tedious to do without lots of automation. What happens when your complex code changes in such a way that you need some extra lemmas but don't know what they are?
First, if some new features are added with associated properties, then some theorems/lemmas related to these properties will have to be added and proven. I don't think that part is problematic, because it's a "local" decision. This work is focused on the change.
The possible problems come from the impact of these changes to existing results. If you need to go and make other changes all over the place it wouldn't be scalable. But then automation and coq hint database can help. In the demo example you referred to Adam adds the lemma as a rewrite hint, and then it's picked by coq automation elsewhere. That's how local changes can automatically be leveraged globally by proof automation in existing proofs, with no changes (ok, not always. But that limits the impact).
See Lean.
It has been used by a "mainstream programmer" to build a RSS feed reader.