In characteristic 0, Kadeishvili has a notion of $C_{\infty}$ algebra which models rational homotopy theory. See the last paragraph of the introduction of his paper arXiv:0811.1655. His point of view is to simply consider $A_{\infty}$ algebras whose operations satisfy a certain property with respect to shuffle maps. So your computer doesn't have to remember any new operations, just check that the old ones are right.

In characteristic $p$, things are probably hopeless.

Added Remark: I just want to make clear that this does not give a "trivial proof" that a commutative dga is formal as a commutative dga if the underlying dga is formal in the "non-commutative" sense. The reason is that when you transfer from cochains from cohomology, you are restricted in the kind of morphisms allowed if you are interested in the commutative theory. So, just as in the answers to this question, there is some work to be done if you want results like that (to be completely honest, there is not yet a proof that I completely understand, so declare myself agnostic).

2 added 688 characters in body

In characteristic 0, Kadeishvili has a notion of $C_{\infty}$ algebra which model models rational homotopy theory. See the last paragraph of the introduction of his paper arXiv:0811.1655. His point of view is to simply consider $A_{\infty}$ algebras whose operations satisfy a certain property with respect to shuffle maps. So your computer doesn't have to remember any new operations, just check that the old ones are right.

In characteristic $p$, things are probably hopeless.

Added Remark: I just want to make clear that this does not give a "trivial proof" that a commutative dga is formal as a commutative dga if the underlying dga is formal in the "non-commutative" sense. The reason is that when you transfer from cochains from cohomology, you are restricted in the kind of morphisms allowed if you are interested in the commutative theory. So, just as in the answers to this question, there is some work to be done if you want results like that (to be completely honest, there is not yet a proof that I completely understand, so declare myself agnostic).

1

In characteristic 0, Kadeishvili has a notion of $C_{\infty}$ algebra which model rational homotopy theory. See the last paragraph of the introduction of his paper arXiv:0811.1655. His point of view is to simply consider $A_{\infty}$ algebras whose operations satisfy a certain property with respect to shuffle maps. So your computer doesn't have to remember any new operations, just check that the old ones are right.

In characteristic $p$, things are probably hopeless.