u/I_am_jake1104

I've been reading about theorem proving, formal methods, symbolic computation, and programming languages, and something keeps bothering me.

They all seem to deal with the same general problem: how abstract mathematics is represented and manipulated by computers.

Things like:

• representing mathematical objects
• proof representation
• symbolic computation
• intermediate representations
• optimization of mathematical structures

These topics seem to exist across several different fields, but I haven't found one that studies them from a unified perspective.

Am I just missing an existing field, or is there a reason these areas evolved separately?

I'd love to hear from people working in PL, theorem proving, or symbolic computation.