You should look into "category theory for programmers" by Bartosz Milewski, or look into the dependently typed languages other people mentioned (Idris, Agda...), or how type theory is replacing set theory as the foundation of mathematics because it makes things computable and is not fundamentally broken (there is an interesting "HoTT book" you can look up that might be relevant).