Jesper Agdakx ♾️Jun 10, 2023

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

Type Systems / Type Theory
25.4%
Runtime Verification (monitoring, instrumentation, ...)
11.7%
Control-Flow and Data-Flow Analysis
13.2%
Abstract Interpretation
4.6%
Formal Verification for Functional Programs (Curry-Howard, dependent types, proof assistants, ...)
10.2%
Formal Logic for Imperative Programs (Hoare logic, separation logic, ...)
9.6%
Automatic Program Verification (model checking, SMT solvers, ...)
8.1%
Operational Semantics (small-step and/or big-step)
8.6%
Semantic Models of Computation (category theory, domain theory, ...)
5.1%
Something else (comment below!)
3.6%
Poll ended at .
Type Theory Forall - #29 Can PL theory make you a better software engineer?

Type Theory Forall is a podcast about Type Theory and Programming Language research in general. We interview relevant people in our field.

RanaldCloustonMar 22, 2023
#CallForPapers #EXPRESS / #SOS 2023 (Combined Workshops on Expressiveness in Concurrency and Structural Operational Semantics) "aims at bringing together researchers interested in the formal semantics of systems and programming concepts, and in the expressiveness of computational models" https://express-sos.github.io/ #concurrency #operationalSemantics #TCS
EXPRESS/SOS 2023

Show threadshape-memory allyApr 19, 2017
@martensitingale I may have painted myself into a corner such that I'm going to have to write a reduction relation that operates on the entire (top-level) program text, so I can pattern-match function bodies out of it rather than building an environment to hold them... this is not the kind of context-with-holes I would have liked #operationalsemantics #mistakes
shape-memory allyApr 19, 2017
because this language doesn't have lambdas, and I'm using a relatively shallow grammar for it, substitution-based reduction of function application gets... interesting #operationalsemantics
shape-memory allyApr 19, 2017
I want something bigsteppy to avoid specifying evaluation order for different elements in a vector to enable optimization #operationalsemantics
shape-memory allyApr 19, 2017
value domain consists of tuples, vectors, ints, bools, where vectors can only hold ints/bools #operationalsemantics
shape-memory allyApr 19, 2017
bouta maybe livetoot writing an #operationalsemantics