Need a running example for my NSF CAREER. Would appreciate some help since I suck at examples, but having one would make my proposal way better.
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:
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.
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.
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).
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.
Please let me know if you have ideas. Can be in any proof assistant language.
Talia Ringer
npub1h2…h3xek
2026-06-10 17:59:01 UTC
Author Public Key
npub1h2yzmr4wgqmehn9fwz0y0tjjh3rwngzpmv6vw6n9gkzv3k0u78zqxh3xekSeen on
wss://relay.momostr.pinkPublished at
2026-06-10 17:59:01 UTCEvent JSON
{
"id": "0d00af2b1671a9c977f6ece052d5bd27b09238d68c42f2037abc0d1a7a0ca1ee",
"pubkey": "ba882d8eae40379bcca9709e47ae52bc46e9a041db34c76a654584c8d9fcf1c4",
"created_at": 1781114341,
"kind": 1,
"tags": [
[
"proxy",
"https://mathstodon.xyz/@TaliaRinger/116727109493559948",
"web"
],
[
"proxy",
"https://mathstodon.xyz/users/TaliaRinger/statuses/116727109493559948",
"activitypub"
],
[
"L",
"pink.momostr"
],
[
"l",
"pink.momostr.activitypub:https://mathstodon.xyz/users/TaliaRinger/statuses/116727109493559948",
"pink.momostr"
],
[
"-"
]
],
"content": "Need a running example for my NSF CAREER. Would appreciate some help since I suck at examples, but having one would make my proposal way better.\n\nIt 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:\n\n1. It is well-motivated and based on actual proof developments I can cite.\n\n2.I can simplify it dramatically when discussing it in the proposal for exemplary purposes.\n\n3. 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.\n\n4. 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).\n\n5. 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.\n\nPlease let me know if you have ideas. Can be in any proof assistant language.",
"sig": "5031da1a1fbb7bb3583c0d5d915281bd1dfc95aeb953aa47de7596e9b28e1d8ed9af04f604d2c9bc660ada1383ed9d1913e2e36428e3190263b33e36caba17aa"
}