See the curry howard isomorphism. Formal logic can be seen as a programming language. In fact, functional programming language are in part based on that correspondence. And some like idris2 and lean4 take it to another level.