Archives of the Caml mailing list > Message from Andrej Bauer

Browse thread

type unsoundness with constraints and polymorphic variants

Stephen Weeks
- Markus Mottl
- Jacques Garrigue
  - Andrej Bauer
    - luc.maranget@i...
    - Jacques Garrigue
      - Christopher L Conway
        
        Michael Hicks
        
        David Teller
        
        Till Varoquaux
        
        Michael Hicks
        
        Mattias EngdegÃ¥ rd
        
        Christopher L Conway
        
        Stefano Zacchiroli

Date:	-- (:)
From:	Andrej Bauer <Andrej.Bauer@f...>
Subject:	Re: [Caml-list] type unsoundness with constraints and polymorphic variants

Out of curiosity, is there a document describing the current ocaml 
typing system, other than the compiler source code?

More generally, what level of formal specification and verification does 
ocaml reach? None, well commented code, a fragment of the language is 
formalized, someone's PhD described the compiler, there is an official 
document describing the compiler, God gave Xavier the type system on Mt 
Blanc, or what?

Andrej