You would probably enjoy this talk by Guy Steele where he discusses the language of mathematics that computer science people use in their papers (Computer Science Metanotation) to talk about other languages. Funnily it's untyped and lacking a rigorous specification... https://www.youtube.com/watch?v=dCuZkaaou0Q
There's a reason why we teach math in kindergarten and proofs in college. There's lots of things that are useful to do without the rigors of rigorous proof.
