hear me out: a #searchengine that understands what you mean (or at least is coachable).

if I look for "heap state program verification" I certainly don't mean the Ohio Home Energy Assistance Program

#ProgramVerification #plt #proglang

There is a real lack of usability studies for doing program verification with dependently typed languages. But broadening our criteria a bit, there are a couple of very useful studies on the usability of other program verification systems such as Dafny, KeY, Frama-C, and others. You can find my attempt so far at a better overview of existing work here: https://researchr.org/bibliography/usability-of-verification-tools/publications. If there's anything that I missed, whether or not it's using dependent types, let me know!

#ProgramVerification #Usability #ProofAssistant

I am listening to the @ttforall podcast with Jimmy Koppel on which parts of CS theory all software engineers should learn about (see also his blog post from 2021 on why programmers should(n't) learn theory). Now I'm curious to learn which parts of "theory" you think are the most useful for a software engineer.

Please boost this so this also finds an audience beyond the types community!

#SoftwareEngineering #Education #TypeTheory #ProgramVerification #AbstractInterpretation #ProofAssistant #HoareLogic #ModelChecking #SMT #OperationalSemantics #CategoryTheory #DomainTheory