Path: csiph.com!xmission!news.snarked.org!border2.nntp.dca1.giganews.com!nntp.giganews.com!news.iecc.com!.POSTED.news.iecc.com!nerds-end From: Martin Ward Newsgroups: comp.compilers Subject: Re: At what point is a language so abstract that it simply cannot be compiled? Date: Tue, 14 May 2019 12:52:44 +0100 Organization: Compilers Central Lines: 68 Sender: news@iecc.com Approved: comp.compilers@iecc.com Message-ID: <19-05-087@comp.compilers> References: <19-05-083@comp.compilers> Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Info: gal.iecc.com; posting-host="news.iecc.com:2001:470:1f07:1126:0:676f:7373:6970"; logging-data="87760"; mail-complaints-to="abuse@iecc.com" Keywords: design Posted-Date: 14 May 2019 12:57:53 EDT X-submission-address: compilers@iecc.com X-moderator-address: compilers-request@iecc.com X-FAQ-and-archives: http://compilers.iecc.com In-Reply-To: <19-05-083@comp.compilers> Xref: csiph.com comp.compilers:2320 My WSL language is a "wide spectrum language" which includes abstract specifications and low-level programming constructs in the same language. At the specification level you can write a specification statement of the form: x := x'.Q where x is a list of variable, x' is the corresponding list of "primed variables" and Q is any formula of infinitary first-order logic. If there is a set of values which can be assigned to x' such that Q becomes true, then these values are assigned to x and the statement terminates. (If there is more than one such set of values, then one is selected nondeterminstically). Otherwise, the statement aborts (does not terminate). For example: := .(x' = x + 1) increments the value in x. Since Q is a formula of infinitary first order logic, the specification statement can be infinitely long. There are formulae for which the solution cannot be computed: for example, the Halting Problem for a Turing machine can be implemented as a specification statement in WSL. The language is used as the basis for my research into program transformations. By using a wide-spectrum language the refinement of a specification into exectuable code is an example of a program transformation, as is the process of reverse-engineering an abstract specification from executable code. A subset of WSL (not including the specification statement) is implemented in the FermaT program transformation system: http://www.gkc.org.uk/fermat.html The FermaT program transformation system is used commercially to migrate assembler code to structured and maintainable functionally equivalent high-level language code. This paper includes an introduction to WSL and transformation theory: "Pigs from Sausages? Reengineering from Assembler to C via FermaT Transformations", M.Ward, Science of Computer Programming, Special Issue on Program Transformation, Vol 52/1-3, pp 213-255, 2004. ISSN 0167-6423 doi:dx.doi.org/10.1016/j.scico.2004.03.007 This paper discusses how the theory can be used to derive algorithms from specifications to give a provably correct implementation: "Provably Correct Derivation of Algorithms Using FermaT" Martin Ward and Hussein Zedan Formal Aspects of Computing, Volume 26, Issue 5, Pages 993–1031, September 2014, ISSN 0934-5043 doi:10.1007/s00165-013-0287-2 Copies of these papers and others are available on my web site: http://www.gkc.org.uk/martin/papers/index.html -- Martin Dr Martin Ward | Email: martin@gkc.org.uk | http://www.gkc.org.uk G.K.Chesterton site: http://www.gkc.org.uk/gkc | Erdos number: 4