PresenceLock is a small Windows utility: a webcam watches for your face, and when you step away and the machine goes idle, it locks the session. A camera-based take on Windows Dynamic Lock.

The face detection is commodity, so it isn’t the point. What matters is that the lock decision is a pure F# function, while everything that touches the world (camera, detector, session lock) sits in a thin C# shell around it. This post is about why that split earns its keep, and what F# gave me for it.

Functional core, imperative shell

The decision core (PresenceLock.Core, in F#) makes every call as a pure function of explicit state, config, time, and events: when to lock, when not to, when to recover. It has no clock of its own and does no I/O. The C# WinForms shell owns everything impure: the camera, face detection, the Win32 session lock, the tray icon, the process lifecycle. It samples the world, calls the core, and executes whatever single action the core returns.

The core’s surface is four functions, and step is the one that matters:

let step (config: PolicyConfig, state: State, ctx: StepContext, event: Event)
    : StepResult

Given the current state, the time, an environment sample, and an event, it returns a new state and exactly one action. No DateTime.Now inside it, no camera handle, no call into Windows.

Why bother

A lock utility is safety-critical in a small, specific way. Lock when you shouldn’t and it’s merely annoying. Fail to lock after you’ve walked away and that’s the security failure the tool exists to prevent. The failure modes that matter are miserable to reproduce by hand in front of a real webcam: a camera that dies mid-session, a glitchy frame that looks like an empty room, a session that was already locked.

Putting the decision in a pure function moves all of that off the webcam and off Windows. The core has no Windows dependency, so I can drive it through every one of those situations as plain function calls, in a container, in milliseconds. The safety-critical logic becomes the easiest code to test, not the hardest.

What F# gave me

The split is the idea. The language is what made it hold up.

Time is a parameter, and it’s typed. Every now is passed in. There are two clocks, and they are different types:

[<Struct>] type MonotonicMs = MonotonicMs of int64   // boot-relative, TickCount64
[<Struct>] type WallClockMs = WallClockMs of int64   // Unix epoch, survives reboots

Monotonic time drives the grace and away timers. Wall-clock time drives only the restart cooldowns, which have to stay meaningful across a reboot. Mixing the two is a classic bug, so the type system refuses it: passing a WallClockMs where a MonotonicMs is expected is a compile error. They’re real struct types rather than [<Measure>] units on purpose. A unit erases to a bare int64 at exactly the C# boundary where the transposition risk lives, and a distinct struct survives it, so the guarantee holds in both languages.

Make the dangerous value unrepresentable, or at least loud. The environment sample the shell passes in on each step (session locked, paused, idle time) is a plain reference record, and deliberately not a struct. As a struct, its zero-initialized default would read as “not paused, not locked, fully idle,” which is exactly the state that says “the user is gone, lock the screen.” That default is reachable through paths no call-site discipline can guard: a dictionary miss, an uninitialized field, Unchecked.defaultof. As a reference type, every one of those paths yields null and throws on first access, so a missing sample fails loud instead of quietly deciding you’ve left. And the action type is a three-case union (do nothing, lock, or restart), so the core cannot emit two actions from one step. The cardinality is the type, not a convention.

The state is opaque. State is a public type, because the shell has to hold one and thread it through, but its representation is internal. The shell can’t construct one, can’t pattern-match it, can’t hand-roll a state that lies. The only way to look inside is snapshot, a read-only projection used for logging and tests. There is exactly one writer of the real state, and it’s the core.

Don’t fold truth you can just re-observe. Whether the session is locked or paused is sampled fresh on every step, never accumulated from events. That’s a scar. An earlier design folded those flags from session-switch events, and a single swallowed edge desynced the belief permanently. The tool thought the session was unlocked long after it wasn’t. Sampled truth can’t drift, because there is nothing to drift from. The core trusts what the shell observed this instant, not a running tally it kept.

Fail toward not locking you out. A bad frame (no frame, or a too-dark one) is treated exactly like seeing your face for the away timer, so a camera hiccup never locks the screen on its own. A truly dead camera surfaces instead as a distinct no-signal status and, past a threshold, asks the shell to restart the process, rather than wedging or silently going blind. Recovery is always a clean process restart, decided by the core and carried out by the shell. In-process camera re-init is never an option, because a wedged capture stack doesn’t reliably recover without one.

Testing a core that can’t touch Windows

Because the core is pure and Windows-free, it gets tested the way pure code should be. There are ordinary xUnit scenario tests and FsCheck property tests over the decision logic. On top of that sits a model-based verification harness: an exhaustive breadth-first explorer over the reachable graph of environment states crossed with abstracted core states, checking the invariants hold everywhere it can reach.

Mutation testing is where the encapsulation pays off again. The core’s state representation is internal, so a mutant (a deliberately broken version, used to check the tests actually catch bugs) can’t reimplement the decision logic from scratch. It has no way to build a State. Its only lever is what it feeds the real start and step, which is exactly the shape of the real bug the harness guards against: the folded-flag desync was never a from-scratch rewrite, it was feeding the right functions the wrong remembered inputs. The encapsulation that makes the shell safe also makes the mutants realistic. (If property and exhaustive testing is your thing, it’s the same instinct behind nelli , my Nim testing engine: different language, same conviction that the core should be the easy part to verify.)

A note on the camera

A tool that watches a webcam should say plainly what it does with the video. Everything runs locally. Frames are read, checked for a face, and dropped. Nothing is stored, and nothing leaves the machine. The camera’s lifecycle (when it’s on, when it’s released) lives in the shell, and the core never sees a pixel, only the labels FaceSeen, NoFace, NoFrame, and DarkFrame.

Takeaway

None of this is exotic F#. It’s records, unions, a couple of single-case struct types, and functions with no side effects. But that small kit is enough to push every decision that matters into a pure core, make the hazards into compile errors, and keep Windows at arm’s length where it belongs. The lock brain ends up the simplest, most-tested code in the project, which for a thing whose job is to lock your screen when you leave is the only way I wanted it.

Code is at github.com/coreyleavitt/presence-lock (Apache-2.0). The design record and the full invariant list live in the repo’s ARCHITECTURE.md.