There are two "cultures" of mathematics in my particular area of interest, namely computational mathematics. I spent an intense year of study reading several h

There are two "cultures" of mathematics in my particular area of interest, namely computational mathematics. I spent an intense year of study reading several hundred papers crossing both cultures. One culture (my "original home culture") is generally referred to as "computer algebra". Here algorithms are developed and favored because they "mostly work". The second culture generally falls under "proof assistance". Here various logic theories are developed and then implemented to support developing proofs as approved by the chosen logic. Of the several hundred papers the only name I can find that crosses both cultures, based on bibliographies from the papers, is James Davenport, a rather clever English chap. https://en.wikipedia.org/wiki/James_H._Davenport https://en.wikipedia.org/wiki/James_H._Davenport I'm wasting my time trying to straddle this gap, striving for a combination I refer to as computational mathematics. The struggle is that the computer algebra culture, being ad-hoc, does not have a way to create proofs of algorithms. The proof assistant culture, being theory-based, does not, in my experience, even permit the discussion of proving algorithms. These two cultures have 25-plus years of parallel development with nearly disjoint biblographies. This seems to align well with Gower's two cultures theory.