guile-user
[Top][All Lists]
Advanced
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: A bit further toward the flamewar

From: Hans Aberg
Subject: Re: A bit further toward the flamewar
Date: Thu, 13 Oct 2011 23:58:23 +0200 
On 13 Oct 2011, at 23:14, Ludovic Courtès wrote:

> Did you know that Coq would only compile a function when it can prove
> that it terminates?  That’s another kind of compiler-supported proof one
> quickly gets used to.

Termination is a non-deducable property. They look at a intuitionistic subset 
of programs.

Hans
reply via email to
[Prev in Thread] Current Thread [Next in Thread]