Differentiable logics (DLs) have increasingly been applied for safe machine learning. In particular, they are useful for giving programming language support to property-driven training. Yet, current DLs either lack important logical properties or hinder model performance. In this project, we develop and study a well-behaved first-order DL designed for safe machine learning, leveraging MathComp’s analysis libraries. To this end, we extend and generalize MathComp with a theory of exponentials and Hölder’s inequality for extended real numbers.