Curry-howard isomorphism in object oriented programming languages I want to get a better intuition for the curry howard isomorphism, and my intuition is mainly based on object oriented programming languages like JavaScript.

So as an example, I am going to formalize the notion of "topological space" in a hypothetical object oriented programming language with dependent type theory and see if it makes sense:

public class TopologicalSpace
{
    BaseSet:Type
    Topology: (BaseSet -&gt; Boolean) -&gt; Boolean 
    public TopologicalSpace(X:Type,T:(X -&gt; 2) -&gt; 2,
         p_axiom1:Axiom,p_axiom2:Axiom2,p_axiom3:Axiom3 )\\constructor
    {
        BaseSet = X;
        Topology = T;
        proof_axiom1 = p_axiom1;
        proof_axiom2 = p_axiom2;
        proof_axiom3 = p_axiom3;
    }

    Axiom1: Topology (function (x:BaseSet) return True) = True 
        AND Topology (function (x:BaseSet) return False) = True \\empty set &amp; domain
              \\ are in topology
    public readonly proof_axiom1:Axiom1    

    Axiom2: \\\etcetcetc
}


Does this approach make sense? Is there a kind of object oriented type theory + curry howard isomorphism like this?
If you only consider terminating functions, then your axiomatisation works :-) Indeed, terminating functions have a resonable notion of equality:
If their return type has decidable equality then the functions have decidable equality.

Regarding your code, it could be rendered in an OOP-like fashion this way

record TopologicalSpace : Set₁ where

  field     
     BaseSet  : Set
     Topology : (BaseSet → Boolean) → Boolean

  Empty    = λ (x : BaseSet) → false
  Universe = λ (x : BaseSet) → true

  field
    axiom1   :       Topology Empty    ≡ true
                AND  Topology Universe ≡ true


This is a real programming language whose functions must always terminate: It is Agda; http://learnyouanagda.liamoc.net/

The source for the code can be found here: https://github.com/alhassy/RandomProgramming/blob/master/Agda/TopologicalSpaces.agda