В самом общем случае поле частных Q определяется для любого целостного кольца R. Но сколь-нибудь производительная на деле арифметика дробей требует наличия алгоритма НОД для R. Ещё более производительная арифметика дробей требует дополнительно выполнения свойства однозначного разложения на простые в R. Выполнение этого свойства необходимо для правильности итога улучшенного способа сложения дробей, тогда как само действие разложения на простые не применяется.
Описываются главные черты программы, которая воплощает все три подхода к арифметике дробей в общем случае, и при этом содержит удостоверение -- полные формальное доказательства
1) правильности каждого из трёх способов сложения, умножения и деления дробей,
2) того, что эти алгоритмы задают структуру поля на Q. Эти определения и доказательства "понимаются" компилятором и автоматически им проверяются до начала исполнения программы.
Эта программа является частью большой библиотеки DoCon-A доказательных программ для алгебры (http://www.botik.ru/pub/local/Mechveliani/docon-A/), написанной докладчиком на языке Agda. Приблизительно можно считать, что Agda есть (чисто функциональный) язык Haskell, расширенный средством зависимых типов.
Два главных преимущества этой системы программирования состоят в том, что
а) алгебраическая область, зависящая от вычисляемого значения, получает адекватное представление,
б) у программиста есть возможность ставить в программу математические (конструктивные) определения и машинно-проверяемые доказательства.