<p>That's a good question! It asks what we expect from types in a typed language.</p>
<p>First note that we can type any programing language with the <em>unitype</em>: just pick a letter, say <code>U</code>, and say that every program has type <code>U</code>. This isn't terribly useful, but it makes a point.</p>
<p>There are many ways to understand types, but from a programmer's point of view the following I think is useful. Think of a type as a <em>specification</em> or a <em>guarantee</em>. To say that <span class="math-container">$e$</span> has type <span class="math-container">$A$</span> is to say that &quot;we guarantee/expect/demand that <span class="math-container">$e$</span> satisfy the property encoded by <span class="math-container">$A$</span>&quot;. Often <span class="math-container">$A$</span> is something simple like <code>int</code>, in which case the property is simply &quot;it's an integer&quot;.</p>
<p>There is no end to how expressive your types can be. In principle they could be any kind of logical statements, they could use category theory and whatnot, etc. For example, dependent types will let you express things like &quot;this function maps lists to list such that the output is a sorted input&quot;. You can go further, at the moment I am listening to a talk on &quot;concurrent separation logics&quot; which allows you to speak about how concurrent programs work with shared state. Fancy stuff.</p>
<p>The art of types in programming language design is one of <strong>balancing expressivity and simplicity</strong>:</p>
<ul>
<li>more expressive types allow us to explain in more detail (to ourselves and to the compiler) what is supposed to be going on</li>
<li>simpler types are easier to understand and can be automated more easily in the compiler.</li>
</ul>
<p>Simplicity is not to be underestimated, as not every programmer has a PhD in theory of programming languages.</p>
<p>So let us come back to your question: how do you know that your type system is <em>good</em>? Well, prove theorems that show your types to be balanced. There will be two kinds of theorems:</p>
<ol>
<li><p>Theorems which say that your types are <em>useful</em>. Knowing that a program has a type should imply some guarantees, for instance that the program won't get stuck (that would be a <em>Safety theorem</em>). Another family of theorems would connect the types to <em>semantic models</em> so that we can start using real math to prove things about our programs (those would be <em>Adequacy theorems</em>, and many others). The unitype above is bad because it has not such useful theorems.</p>
</li>
<li><p>Theorems which say that your types are <em>simple</em>. A basic one would be that it is decidable whether a given expression has a given type. Another simplicity feature is to give an algorithm for inferring a type. Other theorems about simplicity would be: that an expression has at most one type, or that an expression has a principal type (i.e., the &quot;best&quot; one among all types that it has).</p>
</li>
</ol>
<p>It is difficult to be more specific because types are a very general mechanism. But I hope you see what you should shoot for. Like most aspects of programming language design, there is no absolute measure of success. Instead, there is a space of design posibilities, and the important thing is to understand where in the space you are, or want to be.</p>

CC BY-SA 3.0
2017-06-12T09:55:35.427Z
Thank you for that detailed answer! However, I'm still not sure about the answer to my question. As a concrete example, let's take C - a statically typed language with a simple enough type system. If I wrote a typechecker for C, how would I prove that my typechecker is "correct"? How does this answer change if instead I wrote a type checker for Haskell, say HM? How would I now prove "correctness"?
Vivek Ghaisas
CC BY-SA 3.0
2017-06-12T10:24:45.153Z
1. Actually define the type system $T$ for C as a mathematical entity (so that you can prove theorems about it). 2. Implement your typechecker, or describe an algorithm for type checking. 3. Prove the theorem: *If my typechecker checks that $e$ has type $A$ then there is a derivation in the type system $T$ showing that $e$ has type $A$.
Andrej Bauer
CC BY-SA 3.0
2017-06-12T10:25:32.180Z
I would recommend doing 2. and 3. as a combination. Also, have a look at [CompCert](http://compcert.inria.fr).
Andrej Bauer
CC BY-SA 3.0
2017-06-13T09:01:50.730Z
Great answer. One thing I would add is that the literature on type systems often focuses on "soundness" theorems, but another aspect of correctness that one might care about is "completeness" (which seems to be implicit in the OP's "I want my type checker to be able to identify any errors in a piece of code that might occur at runtime"). In particular, in addition to the theorems you mentioned, one might hope to establish: 1. If there is a derivation in the type system $T$ showing that $e$ has type $A$, then the typechecker verifies that $e$ has type $A$, and/or 2. if $e$ does ...
Noam Zeilberger
CC BY-SA 3.0
2017-06-13T09:04:35.333Z
... not have type $A$, then it does not exhibit the expected behavior of an $A$ at runtime (or more simply, if $e$ is not typable, then it goes wrong at runtime). One reason these completeness aspects are sometimes neglected is that they can run into undecidability issues as the type system becomes more expressive (and there is a tradeoff between 1 and 2: as the type system becomes more expressive to catch errors, it becomes more difficult to automate type checking). Still, sometimes it is possible to prove such soundness + completeness theorems, ...
Noam Zeilberger
CC BY-SA 3.0
2017-06-13T09:04:42.817Z
... and I think it is useful to have them in mind as the ideal standard for mathematical correctness.
Noam Zeilberger
CC BY-SA 3.0
2017-06-13T09:08:52.273Z
(I see that wren romano's answer touched on some of this.)
Noam Zeilberger
CC BY-SA 4.0
2017-06-12T09:00:35.923Z
2024-06-06T19:57:30.667Z
2024-06-06T19:57:30.667Z
Andrej Bauer
<p>There are a few different things you could mean by "prove that my typechecker works". Which, I suppose, is part of what your question is asking ;)</p>

<p>One half of this question is proving that your type <em>theory</em> is good enough to prove whatever properties about the language. <a href="https://cstheory.stackexchange.com/a/38406/1808">Andrej's answer</a> tackles this area very well imo. The other half of the question is —supposing the language and its type system are already fixed— how can you prove that your particular type checker does in fact implement the type system correctly? There are two main perspectives I can see taking here.</p>

<p>One is: how can we ever trust that some particular implementation matches its specification? Depending on the degree of assurances you want, you may be happy with a large test suite, or you may want some sort of formal verification, or <a href="https://blog.acolyer.org/2017/05/29/an-empirical-study-on-the-correctness-of-formally-verified-distributed-systems/" rel="noreferrer">more likely a mixture of both</a>. The upside of this perspective is that it really highlights the importance of setting boundaries on the claims you're making: what exactly does "correct" mean? what portion of the code is checked, vs what part is the assumed-correct TCB? etc. The downside is that thinking too hard about this <a href="https://sysadm.equoria.com/images/7/78/Thompson.pdf" rel="noreferrer">leads one down philosophical rabbit holes</a>— well, "downside" if you don't enjoy those rabbit holes.</p>

<p>The second perspective is a more mathematical take on correctness. When dealing with languages in maths we often set up "models" for our "theories" (or vice versa) and then try to prove: (a) everything we can do in the theory we can do in the model, and (b) everything we can do in the model we can do in the theory. (These are <em>Soundness</em> and <em>Completeness</em> theorems. Which one's which depends on whether you "started out" from the syntactic theory or from the semantic model.) With this mindset we can think of your type-checking implementation as being a particular model for the type theory in question. So you'd want to prove this two-way correspondence between what your implementation can do and what the theory says you should be able to do. The upside of this perspective is that it really focuses on whether you've covered all the corner cases, whether your implementation is complete in the sense of not leaving out any programs it should accept as type-safe, and whether your implementation is sound in the sense of not letting in any programs it should reject as ill-typed. The downside is your proof of correspondence is likely to be fairly separated from the implementation itself, so it'll only help prove the gross structure of your implementation is good, it may not help catch subtle implementation bugs.</p>

CC BY-SA 3.0
2017-06-13T08:17:42.447Z
I'm not sure I can agree with "upside of this perspective is that it really focuses on whether you've covered all the corner cases", especially if the model is only sound, but not complete. I'd propose a different perspective: going through a model is a  contingent *proof technique* that you use for various reasons, e.g. because the model is simpler. There is nothing philosophically more dignified about going through a model -- ultimately you want to know about the actual executable and its behaviour.
Martin Berger
CC BY-SA 3.0
2017-06-13T09:20:37.047Z
I thought "model" and "theory" were meant in a broad sense, and wren was just emphasizing the importance of trying to establish a two-way correspondence via a "soundness + completeness theorem". (I also think this is important, and made a comment to Andrej's post.) It's true that in some situations we'll only be able to prove a soundness theorem (or a completeness theorem, depending on your perspective), but having both directions in mind is a useful methodological constraint.
Noam Zeilberger
CC BY-SA 3.0
2017-06-13T09:43:13.713Z
@NoamZeilberger "The question is," said Martin, "whether you can make words mean so many different things."
Martin Berger
CC BY-SA 3.0
2017-06-13T09:46:52.820Z
When I learned about typing systems and programming language semantics, I found the realisation that models are merely proof techniques about operational semantics, rather than ends in themselves, sublimely liberating.
Martin Berger
CC BY-SA 3.0
2017-06-13T09:49:05.827Z
Relating different models through soundness & completeness is an important scientific methodology for the transfer of insight.
Martin Berger
CC BY-SA 3.0
2017-06-14T01:08:50.677Z
wrenromano I'd guess a complete typechecker should accept all *well-typed* programs, not all *type-safe* ones. A program is type-safe if it doesn't go wrong (which is typically undecidable), and is instead well-typed if it has a type according to the given type rules. For a Turing-complete language type-safety is undecidable, so a decidable type system can't accept all type-safe programs. EDIT: I now see @NoamZeilberger addressed a related point in comments to other answers.
Blaisorblade
CC BY-SA 3.0
2017-06-13T03:58:38.993Z
2017-06-13T03:58:38.993Z
wren romano
<p>The question can be interpreted in two ways:</p>

<ul>
<li>Whether the implementation does implement a given typing system $T$?</li>
<li>Whether the typing system $T$ does prevent the errors you think it should?</li>
</ul>

<p>The former is really a question in program verification and has little to
do with typing. Just needs showing that your implementation meets its
specification, see Andrej's answer.</p>

<p>Let me talk about the later question.  As Andrej said, from an
abstract point of view, a typing system seems to enforce properties on
programs. In practise, your typing system $T$ seeks to prevent errors
from happening, meaning that typable programs  should not exhibit the class
of errors of interest. In order to show that $T$ does what you think
it should, you have to do two things.</p>

<ul>
<li><p>First, you formally define what it means for a program to have an
<strong>immediate typing error</strong>. There are many ways this can be defined
-- it's up to you. Typically we want to prevent programs like
<code>2 + "hello"</code>. In other words, you need to define a
subset of programs, call them  <strong>Bad</strong>, that contains exactly the programs with
immediate typing error.</p></li>
<li><p>Then you must prove that programs that are typable can never  evolve into
programs in <strong>Bad</strong>. Let's formalise this. Let  your typing judgement be
$
    \Gamma \vdash M : \alpha.
   $
Recall that that should be read as:
program   $M$ has  type $\alpha$, assuming   the free variables are typed
as given by the environment $\Gamma$.  Then the theorem you want to
prove is:</p>

<p><strong>Theorem.</strong> Whenever $ \Gamma \vdash M : \alpha $ and $M
   \rightarrow \cdots \rightarrow N$ then $N \notin$ <strong>Bad</strong>.</p>

<p>How to prove this theorem depends on the details of the language, the typing system
and your choice of <strong>Bad</strong>.</p></li>
</ul>

<p>One standard way of defining <strong>Bad</strong> is to say: a term $M$ has an
immediate type error if it is neither a value nor has a reduction
step $M \rightarrow N$. (In this case $M$ is often referred to as <em>stuck</em>.)
This only works for small-step operational semantics. 
One standard way of proving the theorem is to show that</p>

<ul>
<li><p>$ \Gamma
\vdash M : \alpha $ and $M \rightarrow N$ together imply $ \Gamma
\vdash N : \alpha $. This is called "subject reduction". It is usually proven by simultaneous induction on the derivation of the typing judgement, and the length of the reductions.</p></li>
<li><p>Whenever $ \Gamma \vdash M : \alpha $   then $M$ is not  in <strong>Bad</strong>.
This is usually also proven by induction on the derivation of the typing judgement.</p></li>
</ul>

<p>Note that not all typing systems have "subject reduction", for example session types. In this case, more sophisticated proof techniques are required.</p>

CC BY-SA 3.0
2017-06-12T21:09:17.097Z
2017-06-13T08:35:37.740Z
2017-06-13T08:35:37.740Z
Martin Berger
<p>I've been programming for several years, but am very unfamiliar with theoretical CS. I've recently been trying to study programming languages, and as part of that, type checking and inference.</p>

<p>My question is, if I try to write a type inference and checking program for a programming language, and I wish to prove that my typechecker works, what exactly is the proof I'm looking for?</p>

<p>In plain language, I want my type checker to be able to identify any errors in a piece of code that might occur at runtime. If I were to use something like Coq to try proving that my implementation is correct, what exactly will this "proof of correctness" be trying to show?</p>

CC BY-SA 3.0
2017-06-12T17:58:15.113Z
Maybe you can clarify if you want to know (1) whether your implementation does implement a given typing system $T$, or (2) whether your typing system $T$ does prevent the errors you think it should? They are different questions.
Martin Berger
CC BY-SA 3.0
2017-06-12T18:27:22.307Z
@MartinBerger: Ah, I seem to have skipped over that difference. My actual question probably meant to ask both.

The context is that I'm trying to build a language, and for it I was writing a typechecker. And people asked me to use a tried and tested algorithm. I was interested in seeing how hard it would be to "prove" the algorithm and typechecker that I was using were "correct". Hence the ambiguity in my question.
Vivek Ghaisas
CC BY-SA 3.0
2017-06-12T18:32:20.083Z
(1) is really a question in program verification and has little to do
with typing. Just needs showing that your implementation meets its
specification.  As to (2), first define what it means to be an
**immediate type error** (e.g. terms like `2 + "hello"` that are
'stuck').  Once this is formalised, you can then prove type soundness
theorem. That means that no typable program can ever evolve into an
immediate type error. Formally, you prove that if a program $M$ is
typable, and for any $n \geq$: if $M$ runs $n$ steps to become $N$,
then $N$ does not have an immediate type error. (1/2)
Martin Berger
CC BY-SA 3.0
2017-06-12T18:32:29.330Z
This is typically
proven by induction on $n$ and on the derivation of the typing
judegement. (2/2)
Martin Berger
CC BY-SA 3.0
2017-06-12T18:45:54.230Z
Thank you! Based on your explanation, it seems like (2) is indeed what I was looking for. Could you please make that an answer? (And maybe add in any details that you think might be useful.) I would accept that as the answer! :)
Vivek Ghaisas
<coq><type-inference><proof-assistants>
What should a proof of correctness for a typechecker actually be proving?
Vivek Ghaisas
# What should a proof of correctness for a typechecker actually be proving?

(Asked by: username_0 on 2017-06-11)

I've been programming for several years, but am very unfamiliar with theoretical CS. I've recently been trying to study programming languages, and as part of that, type checking and inference.

My question is, if I try to write a type inference and checking program for a programming language, and I wish to prove that my typechecker works, what exactly is the proof I'm looking for?

In plain language, I want my type checker to be able to identify any errors in a piece of code that might occur at runtime. If I were to use something like Coq to try proving that my implementation is correct, what exactly will this "proof of correctness" be trying to show?

**Tags:** coq, type-inference, proof-assistants
> **Comments:**
> **username_1**: Maybe you can clarify if you want to know (1) whether your implementation does implement a given typing system $T$, or (2) whether your typing system $T$ does prevent the errors you think it should? They are different questions.  
> **username_0**: @MartinBerger: Ah, I seem to have skipped over that difference. My actual question probably meant to ask both.  The context is that I'm trying to build a language, and for it I was writing a typechecker. And people asked me to use a tried and tested algorithm. I was interested in seeing how hard it would be to "prove" the algorithm and typechecker that I was using were "correct". Hence the ambiguity in my question.  
> **username_1**: (1) is really a question in program verification and has little to do with typing. Just needs showing that your implementation meets its specification.  As to (2), first define what it means to be an **immediate type error** (e.g. terms like `2 + "hello"` that are 'stuck').  Once this is formalised, you can then prove type soundness theorem. That means that no typable program can ever evolve into an immediate type error. Formally, you prove that if a program $M$ is typable, and for any $n \geq$: if $M$ runs $n$ steps to become $N$, then $N$ does not have an immediate type error. (1/2)  
> **username_1**: This is typically proven by induction on $n$ and on the derivation of the typing judegement. (2/2)  
> **username_0**: Thank you! Based on your explanation, it seems like (2) is indeed what I was looking for. Could you please make that an answer? (And maybe add in any details that you think might be useful.) I would accept that as the answer! :)  

---

## 3 answers

### Answer by username_1 on 2017-06-12. Score: 11 | Accepted answer

The question can be interpreted in two ways:

* Whether the implementation does implement a given typing system $T$?
* Whether the typing system $T$ does prevent the errors you think it should?

The former is really a question in program verification and has little to
do with typing. Just needs showing that your implementation meets its
specification, see Andrej's answer.

Let me talk about the later question. As Andrej said, from an
abstract point of view, a typing system seems to enforce properties on
programs. In practise, your typing system $T$ seeks to prevent errors
from happening, meaning that typable programs should not exhibit the class
of errors of interest. In order to show that $T$ does what you think
it should, you have to do two things.

* First, you formally define what it means for a program to have an
  **immediate typing error**. There are many ways this can be defined
  -- it's up to you. Typically we want to prevent programs like
  `2 + "hello"`. In other words, you need to define a
  subset of programs, call them **Bad**, that contains exactly the programs with
  immediate typing error.
* Then you must prove that programs that are typable can never evolve into
  programs in **Bad**. Let's formalise this. Let your typing judgement be
  $
  \Gamma \vdash M : \alpha.
  $
  Recall that that should be read as:
  program $M$ has type $\alpha$, assuming the free variables are typed
  as given by the environment $\Gamma$. Then the theorem you want to
  prove is:

  **Theorem.** Whenever $ \Gamma \vdash M : \alpha $ and $M
  \rightarrow \cdots \rightarrow N$ then $N \notin$ **Bad**.

  How to prove this theorem depends on the details of the language, the typing system
  and your choice of **Bad**.

One standard way of defining **Bad** is to say: a term $M$ has an
immediate type error if it is neither a value nor has a reduction
step $M \rightarrow N$. (In this case $M$ is often referred to as *stuck*.)
This only works for small-step operational semantics.
One standard way of proving the theorem is to show that

* $ \Gamma
  \vdash M : \alpha $ and $M \rightarrow N$ together imply $ \Gamma
  \vdash N : \alpha $. This is called "subject reduction". It is usually proven by simultaneous induction on the derivation of the typing judgement, and the length of the reductions.
* Whenever $ \Gamma \vdash M : \alpha $ then $M$ is not in **Bad**.
  This is usually also proven by induction on the derivation of the typing judgement.

Note that not all typing systems have "subject reduction", for example session types. In this case, more sophisticated proof techniques are required.


---

### Answer by username_2 on 2017-06-12. Score: 23

That's a good question! It asks what we expect from types in a typed language.

First note that we can type any programing language with the *unitype*: just pick a letter, say `U`, and say that every program has type `U`. This isn't terribly useful, but it makes a point.

There are many ways to understand types, but from a programmer's point of view the following I think is useful. Think of a type as a *specification* or a *guarantee*. To say that $e$ has type $A$ is to say that "we guarantee/expect/demand that $e$ satisfy the property encoded by $A$". Often $A$ is something simple like `int`, in which case the property is simply "it's an integer".

There is no end to how expressive your types can be. In principle they could be any kind of logical statements, they could use category theory and whatnot, etc. For example, dependent types will let you express things like "this function maps lists to list such that the output is a sorted input". You can go further, at the moment I am listening to a talk on "concurrent separation logics" which allows you to speak about how concurrent programs work with shared state. Fancy stuff.

The art of types in programming language design is one of **balancing expressivity and simplicity**:

* more expressive types allow us to explain in more detail (to ourselves and to the compiler) what is supposed to be going on
* simpler types are easier to understand and can be automated more easily in the compiler.

Simplicity is not to be underestimated, as not every programmer has a PhD in theory of programming languages.

So let us come back to your question: how do you know that your type system is *good*? Well, prove theorems that show your types to be balanced. There will be two kinds of theorems:

1. Theorems which say that your types are *useful*. Knowing that a program has a type should imply some guarantees, for instance that the program won't get stuck (that would be a *Safety theorem*). Another family of theorems would connect the types to *semantic models* so that we can start using real math to prove things about our programs (those would be *Adequacy theorems*, and many others). The unitype above is bad because it has not such useful theorems.
2. Theorems which say that your types are *simple*. A basic one would be that it is decidable whether a given expression has a given type. Another simplicity feature is to give an algorithm for inferring a type. Other theorems about simplicity would be: that an expression has at most one type, or that an expression has a principal type (i.e., the "best" one among all types that it has).

It is difficult to be more specific because types are a very general mechanism. But I hope you see what you should shoot for. Like most aspects of programming language design, there is no absolute measure of success. Instead, there is a space of design posibilities, and the important thing is to understand where in the space you are, or want to be.

> **Comments:**
> **username_0**: Thank you for that detailed answer! However, I'm still not sure about the answer to my question. As a concrete example, let's take C - a statically typed language with a simple enough type system. If I wrote a typechecker for C, how would I prove that my typechecker is "correct"? How does this answer change if instead I wrote a type checker for Haskell, say HM? How would I now prove "correctness"?  
> **username_2**: 1. Actually define the type system $T$ for C as a mathematical entity (so that you can prove theorems about it). 2. Implement your typechecker, or describe an algorithm for type checking. 3. Prove the theorem: *If my typechecker checks that $e$ has type $A$ then there is a derivation in the type system $T$ showing that $e$ has type $A$.  
> **username_2**: I would recommend doing 2. and 3. as a combination. Also, have a look at [CompCert](http://compcert.inria.fr).  
> **username_3**: Great answer. One thing I would add is that the literature on type systems often focuses on "soundness" theorems, but another aspect of correctness that one might care about is "completeness" (which seems to be implicit in the OP's "I want my type checker to be able to identify any errors in a piece of code that might occur at runtime"). In particular, in addition to the theorems you mentioned, one might hope to establish: 1. If there is a derivation in the type system $T$ showing that $e$ has type $A$, then the typechecker verifies that $e$ has type $A$, and/or 2. if $e$ does ...  
> **username_3**: ... not have type $A$, then it does not exhibit the expected behavior of an $A$ at runtime (or more simply, if $e$ is not typable, then it goes wrong at runtime). One reason these completeness aspects are sometimes neglected is that they can run into undecidability issues as the type system becomes more expressive (and there is a tradeoff between 1 and 2: as the type system becomes more expressive to catch errors, it becomes more difficult to automate type checking). Still, sometimes it is possible to prove such soundness + completeness theorems, ...  
> **username_3**: ... and I think it is useful to have them in mind as the ideal standard for mathematical correctness.  
> **username_3**: (I see that wren romano's answer touched on some of this.)  

---

### Answer by username_4 on 2017-06-13. Score: 5

There are a few different things you could mean by "prove that my typechecker works". Which, I suppose, is part of what your question is asking ;)

One half of this question is proving that your type *theory* is good enough to prove whatever properties about the language. [Andrej's answer](https://cstheory.stackexchange.com/a/38406/1808) tackles this area very well imo. The other half of the question is —supposing the language and its type system are already fixed— how can you prove that your particular type checker does in fact implement the type system correctly? There are two main perspectives I can see taking here.

One is: how can we ever trust that some particular implementation matches its specification? Depending on the degree of assurances you want, you may be happy with a large test suite, or you may want some sort of formal verification, or [more likely a mixture of both](https://blog.acolyer.org/2017/05/29/an-empirical-study-on-the-correctness-of-formally-verified-distributed-systems/). The upside of this perspective is that it really highlights the importance of setting boundaries on the claims you're making: what exactly does "correct" mean? what portion of the code is checked, vs what part is the assumed-correct TCB? etc. The downside is that thinking too hard about this [leads one down philosophical rabbit holes](https://sysadm.equoria.com/images/7/78/Thompson.pdf)— well, "downside" if you don't enjoy those rabbit holes.

The second perspective is a more mathematical take on correctness. When dealing with languages in maths we often set up "models" for our "theories" (or vice versa) and then try to prove: (a) everything we can do in the theory we can do in the model, and (b) everything we can do in the model we can do in the theory. (These are *Soundness* and *Completeness* theorems. Which one's which depends on whether you "started out" from the syntactic theory or from the semantic model.) With this mindset we can think of your type-checking implementation as being a particular model for the type theory in question. So you'd want to prove this two-way correspondence between what your implementation can do and what the theory says you should be able to do. The upside of this perspective is that it really focuses on whether you've covered all the corner cases, whether your implementation is complete in the sense of not leaving out any programs it should accept as type-safe, and whether your implementation is sound in the sense of not letting in any programs it should reject as ill-typed. The downside is your proof of correspondence is likely to be fairly separated from the implementation itself, so it'll only help prove the gross structure of your implementation is good, it may not help catch subtle implementation bugs.

> **Comments:**
> **username_1**: I'm not sure I can agree with "upside of this perspective is that it really focuses on whether you've covered all the corner cases", especially if the model is only sound, but not complete. I'd propose a different perspective: going through a model is a  contingent *proof technique* that you use for various reasons, e.g. because the model is simpler. There is nothing philosophically more dignified about going through a model -- ultimately you want to know about the actual executable and its behaviour.  
> **username_3**: I thought "model" and "theory" were meant in a broad sense, and wren was just emphasizing the importance of trying to establish a two-way correspondence via a "soundness + completeness theorem". (I also think this is important, and made a comment to Andrej's post.) It's true that in some situations we'll only be able to prove a soundness theorem (or a completeness theorem, depending on your perspective), but having both directions in mind is a useful methodological constraint.  
> **username_1**: @NoamZeilberger "The question is," said Martin, "whether you can make words mean so many different things."  
> **username_1**: When I learned about typing systems and programming language semantics, I found the realisation that models are merely proof techniques about operational semantics, rather than ends in themselves, sublimely liberating.  
> **username_1**: Relating different models through soundness & completeness is an important scientific methodology for the transfer of insight.  
> **username_5**: wrenromano I'd guess a complete typechecker should accept all *well-typed* programs, not all *type-safe* ones. A program is type-safe if it doesn't go wrong (which is typically undecidable), and is instead well-typed if it has a type according to the given type rules. For a Turing-complete language type-safety is undecidable, so a decidable type system can't accept all type-safe programs. EDIT: I now see @NoamZeilberger addressed a related point in comments to other answers.  

---

