* On Thu, Feb 12 2009, chromatic wrote:
> It's trivial to write a type-safe Haskell program which does not violates
> mathematical laws tought to fifth graders and which never terminates. I can
> do it in fewer than ten lines of code.
Wait, you need ten lines for this? I would just say "print [1
* On Thu, Feb 12 2009, Michael G Schwern wrote:
> chromatic wrote:
>> On Thursday 12 February 2009 14:09:41 Michael G Schwern wrote:
>>
>>> I hope somebody writes a provable kernel.
>>
>> Why? It would be practically useless unless they proved all cases of input
>> (user and hardware), in which ca
On Thu, Feb 12, 2009 at 02:09:41PM -0800, Michael G Schwern wrote:
> For day-to-day (or even
> week-to-week) work, testing isn't going anywhere.
It's too late for me to be writing anything at all really, but here's just a
couple of thoughts on
On Thursday 12 February 2009 16:19:55 Michael G Schwern wrote:
> chromatic wrote:
> > Why? It would be practically useless unless they proved all cases of
> > input (user and hardware), in which case it would only be practically
> > useless for every case which lacks complete proofs.
> I'm no e
chromatic wrote:
> On Thursday 12 February 2009 14:09:41 Michael G Schwern wrote:
>
>> I hope somebody writes a provable kernel.
>
> Why? It would be practically useless unless they proved all cases of input
> (user and hardware), in which case it would only be practically useless for
> every
Michael G Schwern writes:
> Which brings us back to Haskell. What if you wrote an operating
> system and compiler, from the bottom up, in a functional programming
> language?
Does not neccessarily need to be FP. See, for example, vFiasco
http://os.inf.tu-dresden.de/vfiasco/ for a C++ microkernel
On Thursday 12 February 2009 14:09:41 Michael G Schwern wrote:
> I hope somebody writes a provable kernel.
Why? It would be practically useless unless they proved all cases of input
(user and hardware), in which case it would only be practically useless for
every case which lacks complete proo
Gabor Szabo wrote:
> Following a blog entry of David A. Wheeler I arrived to the
> web page of Open Proofs: http://www.openproofs.org/ he created.
>
> In short, as I did not understand much, there are tools to mathematically
> prove that a certain program does something or does not do something.
>
Following a blog entry of David A. Wheeler I arrived to the
web page of Open Proofs: http://www.openproofs.org/ he created.
In short, as I did not understand much, there are tools to mathematically
prove that a certain program does something or does not do something.
Unfortunately most of these t
