Weak higher categories can be difficult to work with algebraically, with the weak structure potentially leading to considerable bureaucracy. Conjecturally, every weak $\infty$-category is equivalent to a "semistrict" one, in which unitors and associators are trivial; such a setting might reduce the burden of constructing large proofs. In this talk, I will present the proof assistant homotopy.io, which allows direct construction of composites in a finitely-generated semistrict $(\infty,\infty)$-category. The terms of the proof assistant have an interpretation as string diagrams, and interaction with the proof assistant is entirely geometrical, by clicking and dragging with the mouse, completely unlike traditional computer algebra systems. I will give an outline of the underlying theoretical foundations, and demonstrate use of the proof assistant to construct some nontrivial homotopies, rendered in 2d, 3d, and in 4d as movies. I will close with some speculations about the possible interaction of such a system with more traditional type-theoretical approaches. (Joint work with Nathan Corbyn, Calin Tataru, Lukas Heidemann, Nick Hu and David Reutter.)