Lightweight Static Guarantees

> Morris' old ideas do indeed work. Why don't we use them?

Because we are lazy or overworked?

The last time I wrote C, I had asan and ubsan and valgrind running in CI.

I'm a big fan of giving more feedback to developers at compile-time. A while back I wrote a Java library that makes it easy to add static checks that would otherwise be runtime errors. Link in case someone finds it useful: https://github.com/overstock/annotation-constraints

The verification question is somewhat handwaved in the linked article, but in fact we are now in a position to verify some of this stuff mechanically. Unsurprisingly, the "branding" techniques work, but in type systems that have any amount of subtyping the argument for why they work is subtle and they may not work in all cases.

Also based on the idea of lightweight static checks and dependent types in existing ML languages: https://notebooks.azure.com/allisterb/projects/sylvester/htm...

there are lots of properties app devs & library authors want to verify statically and languages aren't doing a good job of making this easy

JS (for example) has a bunch of 3rd-party type checkers (typescript, flow), and they're huge projects. And flow is even written in ocaml.

I've written static verification of non-type properties when my team absolutely needed it and it's never easy -- even things like AST walking can be rough and non-standard.

Would def try a language that had BYO static checks as a first-class concepts. Code generation is the closest thing to this IMO in widely used languages and even that is clunky in most places (go:generate, I'm looking at you).