> Currently, there's lot of philosophical discussion on ethics, but little of solid decisions and conclusions from these discussions; all the discussion is still at the stage of increasing ambiguity and introducing hypotheses instead of increasing our knowledge about reality by eliminating and discarding most of these hypotheses.

I think greater use of formal methods could really help with this. Imagine if there was e.g. a Coq library containing formalisations of all the common systems of axioms, and the various conclusions that followed from them. It would make exploration so much easier.