Need a running example of a formal verification or math formalization project (using proof assistants) for my NSF CAREER. Would appreciate some public brainstorming since I am not good at examples, but having one would make my proposal way better. Thread below.
Users appreciate the discussion of formal verification examples for an NSF CAREER proposal because it supplies citable references and serves the research community.
It should be a verification or formal math project (described at a very high level, like "suppose we are verifying a compiler from our own language to CompCert CLight" or whatever) with the following (IME very common) properties:
Need a running example of a formal verification or math formalization project (using proof assistants) for my NSF CAREER. Would appreciate some public brainstorming since I am not good at examples, but having one would make my proposal way better. Thread below.
@TaliaRinger
Please let me know if you have ideas. Can be in any proof assistant language. I want to frame my proposal (which I already have very strong and specific ideas for) around an example like this, but I need to talk to people to figure out exactly what it should be.
5. It is something that it would make sense to collaborate on with a sizable group of collaborators, who may be opinionated about questions of proof engineering best practices, or about best practices specific to that domain.
@TaliaRinger This example is kind of embarrassing that it hasn’t been done already. Suppose you want to extend CakeML, a formally verified ML compiler, so that you can print out the value of a floating point number.
@TaliaRinger For example, the memory safety properties of the CHERI architecture were formally verified. At early stages of the development process, there were proposals for new instructions, usually to make the operating system run faster.
1. It is well-motivated and based on actual proof developments I can cite.
2. I can simplify it dramatically when discussing it in the proposal for exemplary purposes.
It should be a verification or formal math project (described at a very high level, like "suppose we are verifying a compiler from our own language to CompCert CLight" or whatever) with the following (IME very common) properties:
3. The programs, definitions, and theorem statements are not all known in advance---it makes sense for the proof engineer to figure those things out as they go.
1. It is well-motivated and based on actual proof developments I can cite.
2. I can simplify it dramatically when discussing it in the proposal for exemplary purposes.
@TaliaRinger I've been formalizing the math used to train MNIST (and much larger networks) in lean4: https://brettkoonce.github.io/lean4-mlir/blueprint/
5. It is something that it would make sense to collaborate on with a sizable group of collaborators, who may be opinionated about questions of proof engineering best practices, or about best practices specific to that domain.
4. It depends on a custom library and/or exists in a specific domain that uses a lot of custom definitions and custom styles (but not a monorepo like mathlib).
@TaliaRinger You might have some high-level property known in advance: “if I convert a float to a string then back to a float, I get the original value, unless it’s NaN”, but you will probably need to invent definitions as you describe what the string representation of a float is.
@TaliaRinger So, you need to check that each new instruction you add does not break the security model in some way.
4. It depends on a custom library and/or exists in a specific domain that uses a lot of custom definitions and custom styles (but not a monorepo like mathlib).
3. The programs, definitions, and theorem statements are not all known in advance---it makes sense for the proof engineer to figure those things out as they go.
@lastland0 I'll take a look! Do you have any examples of (3)---places where you weren't certain what definitions to write or what theorems to state in advance, and had to figure those things out as you went?
@lastland0 Oh cool! OK, will read, it is good that is discussed because I can cite it instead of relying on lore
@lastland0 Definitely doing a service for the community with that discussion!
@TaliaRinger Are you looking for existing projects, or potential projects?
I just joined o9 and I'm seriously looking at specifying/verifying code for describing enterprise planning processes, but it's still at a stage where I don't know if it will make sense or be entirely viable.
@TaliaRinger I'm doing a SQL statement equivalency checker in Lean4. Could also do Datalog.
@TaliaRinger To do this, you going to need to develop some kind of formalized theory of how IEEE 754 represents floating point values as sequences of characters.
@TaliaRinger A math formalization project with these requirements seems hard to think of undirected, but what about verification of permissions systems (like for data access)? They often have correctness problems, I know it's a vaguely worked upon subject.
@TaliaRinger Even if it makes sense I'm not sure it fits what you're looking for.
Need a running example of a formal verification or math formalization project (using proof assistants) for my NSF CAREER. Would appreciate some public brainstorming since I am not good at examples, but having one would make my proposal way better. Thread below.