PHP Finally Getting a Formal Specification

itwbennett (1594911) writes "Despite becoming one of the most widely used programming languages on the Web, PHP didn't have a formal specification — until now. Facebook engineer and PHP core contributor Sara Golemon announced the initiative at OSCON earlier this month, and an initial draft of the specification was posted Wednesday on GitHub."

Comments

Re:Formal specifications are pretty useless for th

[gweihir]

Yes, very much so. Most languages do not have formal specifications.

Re:Formal specifications are pretty useless for th

[Anonymous Coward]

Not really.
If you don't have a formal specification and you have two implementations that do different things, there is no way to know which is correct.
Besides, not having a specification is what led to PHP being such an ad-hoc mess in the first place.

Re:Formal specifications are pretty useless for th

[gweihir]

I should also add that what they are doing is at best a "semi-formal specification". Still pretty clunky.

its why devs cringe.

[nimbius]

As a devops (christ i hate that word.) engineer, the fact that the lack of a formal specification was overlooked for 20 years has been and is currently a big red flag for any legitimate software project. It was the knee-jerk reaction to Jakarta/Tomcat/Struts and ultimately java based, head first strict-type coding that turned programming projects into concentration camps. It emerged during a period when programmers were still struggling to determine how to present content to users sustainably, instead of having to write the entire page in perl. IMHO this is too little too late.

This is entirely opinion, but having lived with web n.x for 15 years, Python has emerged a juggernaut to contend with in RESTful coding environments. it learned from PHP's mistakes and walked away from perl with a firm understanding of what made it uncomfortable from the debug standpoint. things like CherryPy, TurboGears, pylons and even pecan can turn a proof of concept in a day, and can easily and quickly be scaled across the infrastructure.

Re:its why devs cringe.

[OzPeter]

Python has emerged a juggernaut to contend with in RESTful coding environments.

Putting aside the whole whitespace debate(*), I'm pretty sure that python has its own list of issues. Maybe not to the same extent as PHP, but they exist.

* For which I personally do have trouble with python - I want the computer to bend to my will, not the other way around.

Re:its why devs cringe.

[ShadowRangerRIT]

Most high level scripting languages (can't speak for PHP, but it's true for Perl, Ruby and Python) implement simple user defined objects as dictionaries. That said, the lookup cost, while obviously much higher than pre-compiled v-tables, are not as expensive as you might imagine; attribute access uses interned strings, and strings cache their hash code on first hash. If you don't actually have to recompute the hash, and equality checks are (for attribute lookup) a simple reference identity test, the CPU costs are basically nil, you just have the issue of page faulting due to "random" access into the hash table (and Python at least optimizes for that case; the collision chaining algorithm in recent versions of Python tries to chain into the same cache line if it can, alternating with chains by "long steps" to avoid issues with consecutive hash codes).

Stuff that kills Python performance includes: Minimal optimization of code by the byte code compiler, and none by the byte code interpreter (while each hash table lookup is cheap, a loop will perform it over and over again, even if you're accessing the same attribute on the same object, because the compiler and interpreter aren't sophisticated enough to recognize what's happening); inability to parallelize CPU bound tasks using threads thanks to the GIL; lack of "primitive" types, so even basic math involves substantial memory allocator overhead and memory fragmentation, etc.

TL;DR: Python's performance problems aren't primarily a result of hash tables.

At last

[geminidomino]

I wonder if my favorite bug/misfeature will make the cut and be enshrined forever, because it's *fun* when a successful database instruction throws an exception.

PHP Finally Getting a Formal Specification

[NoNonAlphaCharsHere]

Unfortunately, it's written in PHP, so there's some disagreement about WHAT is says.

Re:PHP Finally Getting a Formal Specification

[NoNonAlphaCharsHere]

Actually SpecificationFormal($PHP) automagically converted $PHP to Perl and returned false. No-one is sure WHY, but that's the way it works.

Re:PHP Finally Getting a Formal Specification

[Megane]

I'll just wait for them to replace php_specification() with real_php_specification() ... or is it php_real_specification() ?

Re:Formal specifications are pretty useless for th

[Tailhook]

Yes, which is probably why this is coming from a Facebook engineer. PHP is pretty central to Facebook and Facebook has been re-implementing PHP for many years now. Facebook created a PHP to C++ translator (HPHPc) which has since been deprecated in favor of a new PHP virtual machine; HHVM. So Naturally formalizing PHP is of great interest to Facebook.

Six identifiable bullet points

[tepples]

Let's play Hegelian dialectic: Thesis The "fractal" rant Antithesis The "hardly" rebuttal Synthesis Six identifiable bullet points

Re:Engineer?

[OzPeter]

Facebook engineer and PHP core contributor....

My father in law in an actual engineer

As an actual engineer as well, this sort of inflating of titles is a peeve of mine right now. It makes job searches nigh impossible as every position out there has the word engineer in them, and all recruiters seem to be doing nowadays is matching keywords - sort I keep getting emails about 'engineer this' and 'engineer that', when they are totally irrelevant to any sort of genuine engineering position.

Re:Formal specifications are pretty useless for th

[Daniel Hoffmann]

A formal specification is useful for the implementers of the languages to guarantee that your code runs the same across all implementations. It is pretty important. It should define all use cases possible and highlighting the "undefined" use cases.

Re:How did we get along for so many years without

[ruir]

Maybe, maybe not. Will we have now a PHP compiler to binary code?

Re:Formal specifications are pretty useless for th

[rockmuelle]

Actually, neither C nor C++ have formal specifications. They both have very well defined and curated standards documents that can be called specifications (without the formal part), but neither has a proper formal specification.

-Chris

Full specification text:

[goodmanj]

PHP Formal Specification:

1) Don't use PHP.

Re:Full specification text:

[lgw]

PHP Formal Specification:

1) Don't use PHP.

No wonder you're getting modded down if you think that's a formal specification! C'mon:

1. Abstract.

Don't use PHP.

2. Conventions used in this document.

The key words "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL NOT",
"SHOULD", "SHOULD NOT", "RECOMMENDED", "MAY", and "OPTIONAL" in this
document are to be interpreted as described in RFC-2119

3. Normative Guidance for the Use of PHP

One MUST NOT use PHP.

Re:Formal specifications are pretty useless for th

[CrashNBrn]

Also, Hack:a new (Open Source) programming language for HHVM

Hack, a programming language developed for HHVM that interoperates seamlessly with PHP.
Hack reconciles the fast development cycle of PHP with the discipline provided by static typing, while adding many features commonly found in other modern programming languages.

An open source version of Hack is available at http://hacklang.org/ as part of the HHVM runtime platform, which supports both Hack and PHP.

Also, FBIDE (a web-based Hack development environment) was presented at Facebook's Hack Developer Day,

Joel B. and I introduced Facebook's web-based Hack development environment, known internally as âoeFBIDE.â The Hack type checker is compiled to JavaScript, so all Hack language checking is done very fast, client-side. Features of FBIDE include autocomplete, an integrated debugger, quick file and code search, and other pretty cool things. FBIDE has been a great success internally at Facebook. At a company where vim and emacs are the dominant choices for development, a large percentage of Facebook engineers are using FBIDE, and the number is growing quickly. We believe FBIDE will be useful to Hack developers outside of Facebook, allowing them to productively become familiar with the language, so we're working on plans to make it more widely available â" hopefully toward the end of summer 2014.

Re:Existing app

[Zero__Kelvin]

Reimplementation, or more accurately, implementing it properly for the first time.

Re:Formal specifications are pretty useless for th

[gweihir]

A formal specification is a specification done in a formal specification language. There is no other meaning of that term. The people claiming they are doing a "formal" specification likely confused this with "exact". These two concepts are orthogonal. A formal specification can be inexact (or even unsound), while an informal specification can be exact (and sound).

A "formal standard" is something else, it usually refers to a more-or-less exact and complete _informal_ specification that is uniquely identified by its designation. The main difference is that in theory, you could check a formal specification for soundness using an automated theorem prover. Or you could automatically generate a compiler from it. An informal (but possibly exact) specification does not allow that, as it needs a human in the loop.

Re:Formal specifications are pretty useless for th

[lgw]

Understanding implies the ability to explain ones position, not merely assert it. You come off like those clowns who go on about proofs of program correctness, but perhaps that's a mistaken impression

Can you give an example of a formal language spec? Are you talking about an actual set of formal transforms to object code or somesuch?

BTW, set-ups like a C compiler written in C are very much in line with Godel statements. There certainly exists source code for which the question "does this compiler compile this source code correctly" cannot have a useful answer as a formal proof (and the examples easiest to contrive would include the compiler itself in said source code).