4 ms·

I'm optimistic that improved proof search using modern AI can make working with dependent type systems much more productive and practical. A future programmer

by rictic 2y ago

I'm optimistic that improved proof search using modern AI can make working with dependent type systems much more productive and practical. A future programmer may be spending more time formally describing the invariants of the system.