* proving a file system
@ 2020-04-26 21:15 ori
2020-04-26 21:57 ` [9front] " ori
0 siblings, 1 reply; 2+ messages in thread
From: ori @ 2020-04-26 21:15 UTC (permalink / raw)
To: 9front
So, I'm finally back to working on gefs, and I was thinking that it'd
be good to prove the invariants -- but I've got no experience with coq,
isabelle/HOL, or whatever I should be using. I'd want to prove that the
insertion/deletion/... is crash safe and concurrency safe, if I can do
that sanely.
Currently a little ways off from getting something that needs proving,
but curious if you think this would be worthwhile, and if you'd have
some interest in helping out.
^ permalink raw reply [flat|nested] 2+ messages in thread
* Re: [9front] proving a file system
2020-04-26 21:15 proving a file system ori
@ 2020-04-26 21:57 ` ori
0 siblings, 0 replies; 2+ messages in thread
From: ori @ 2020-04-26 21:57 UTC (permalink / raw)
To: ori, 9front
> So, I'm finally back to working on gefs, and I was thinking that it'd
> be good to prove the invariants -- but I've got no experience with coq,
> isabelle/HOL, or whatever I should be using. I'd want to prove that the
> insertion/deletion/... is crash safe and concurrency safe, if I can do
> that sanely.
>
> Currently a little ways off from getting something that needs proving,
> but curious if you think this would be worthwhile, and if you'd have
> some interest in helping out.
...oops, didn't mean to send it to the 9front list.
Anyways, if people *are* interested, feel free to ping me; expecting that
it'll be a few weeks before there's have something to talk about seriously.
^ permalink raw reply [flat|nested] 2+ messages in thread
end of thread, other threads:[~2020-04-26 21:57 UTC | newest]
Thread overview: 2+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2020-04-26 21:15 proving a file system ori
2020-04-26 21:57 ` [9front] " ori
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).