Loading ...
Sorry, an error occurred while loading the content.

Messages List

5026

Re: Where's formal proof of Haskell's claim to...?

]> Where's formal proof of Haskell's claim to be able to avoid the need to ]> tell the machine what to do step-by-step, and just provide it with a ]>
chris glur
Mar 9
#5026
 
5025

Re: Where's formal proof of Haskell's claim to...?

... [...] ... Do you have a specific quote in context for the claim for better understanding of the question? The general theory is the Church–Rosser
Michael Haufe
Feb 23
#5025
 
5024

Where's formal proof of Haskell's claim to...?

be able to avoid the need to tell the machine what to do step-by-step, and just provide it with a , and allow it to workout/search
chris glur
Feb 23
#5024
 
5023

Re: Formal proofs via 'joy' or any system?

... There are more than just claims, you'll be happy to know! Richard Bird and Jeremy Gibbons have done a lot of work on this topic. Bird's "The Algebra of
John Nowak
Nov 18, 2014
#5023
 
5022

Formal proofs via 'joy' or any system?

Cc: ETHO forum. Re. "rock solid"/reliable software: Ada had that declared aim. Is it still alive? Wirth advocated simplicity; if the whole-picture is small
chris glur
Nov 17, 2014
#5022
 
5021

Re: Must have SINGLE input/Arg.

... Verily so. I'm reminded of the teacher who asked his class to determine the most efficient path to move an object from the top of his dest to a far upper
Don Groves
Sep 8, 2014
#5021
 
5020

Re: Must have SINGLE input/Arg.

chris glur crglur@... [concatenative] ... No, it's because I follow language design in general. It really, really isn't concatenative. ... -Wm
William Tanksley, Jr
Sep 8, 2014
#5020
 
5019

Re: Must have SINGLE input/Arg.

... Yes, when I mistakenly though that I needed MicroSoft to connect a 3Gdongle, and bought a M$ device, I got the impression that M$ finally realised the
chris glur
Sep 8, 2014
#5019
 
5018

Re: Must have SINGLE input/Arg.

chris glur crglur@... [concatenative] ... We have an almost impossibly broad challenge, Chris -- we're taking a practical language that exists in only a
William Tanksley, Jr
Aug 26, 2014
#5018
 
5017

Re: Must have SINGLE input/Arg.

Re. refining the TextToSpeech system by just adding extra stages of composition/data-transformation: it was quiet nice to be able to lie down after a strenuous
chris glur
Aug 26, 2014
#5017
 
5016

Re: Must have SINGLE input/Arg.

... ==> SCREW YOU !! Readers of this forum are dispersed over the globe, with different knowledge/experience backgrounds, using different OSs ...... What [if
chris glur
Aug 26, 2014
#5016
 
5015

Re: Must have SINGLE input/Arg.

Lot's of fun stuff to read. thanks. I guess I was thinking more of the simple inductive reasoning I tend to use with haskell code that uses bottom as a base
John Meacham
Aug 13, 2014
#5015
 
5014

Re: Must have SINGLE input/Arg.

Im not sure that is the case. As I understand it it should be possible even for a total language to reason about infinite structures. Here's a paper
John Nilsson
Aug 12, 2014
#5014
 
5013

Re: Must have SINGLE input/Arg.

... I don't think this is true. It's possible to define and formally reason about infinite data structures in Coq by defining codata, and Coq has no bottom.
John Nowak
Aug 12, 2014
#5013
 
5012

Re: Must have SINGLE input/Arg.

An issue with no bottom is that having it is necessary to properly reason about infinite data structures. Now, as to whether you actually want infinite data
John Meacham
Aug 11, 2014
#5012
 
View First Topic Go to View Last Topic
Loading 1 - 15 of total 5,026 messages