372 lines
14 KiB
Markdown
372 lines
14 KiB
Markdown
[Source](https://www.microsoft.com/en-us/research/publication/specification-language-typed/?from=http%3A%2F%2Fresearch.microsoft.com%2Fen-us%2Fum%2Fpeople%2Flamport%2Fpubs%2Flamport-types.pdf "Permalink to Should Your Specification Language Be Typed? - Microsoft Research")
|
|
|
|
# Should Your Specification Language Be Typed? - Microsoft Research
|
|
|
|
Try Microsoft Edge A fast and secure browser that's designed for Windows 10 No thanks Get started
|
|
|
|
This site uses cookies for analytics, personalized content and ads. By continuing to browse this site, you agree to this use. [Learn more][1]
|
|
|
|
[ ![][2] Microsoft ][3]
|
|
|
|
Research
|
|
|
|
* [Microsoft 365][4]
|
|
* [Azure][5]
|
|
* [Office 365][6]
|
|
* [Dynamics 365][7]
|
|
* [SQL][8]
|
|
* [Windows 10][9]
|
|
* More
|
|
* Products & Services
|
|
* [Windows Server][10]
|
|
* [Enterprise Mobility + Security][11]
|
|
* [Power BI][12]
|
|
* [Teams][13]
|
|
* [Visual Studio][14]
|
|
* [Surface for Business][15]
|
|
* Emerging Technologies
|
|
* [AI][16]
|
|
* [Internet of Things][17]
|
|
* [Azure Cognitive Services][18]
|
|
* [Quantum][19]
|
|
* [Research][20]
|
|
* Developer & IT
|
|
* [Docs][21]
|
|
* [TechNet][22]
|
|
* [Developer Network][23]
|
|
* [Windows Dev Center][24]
|
|
* [Windows IT Pro Center][25]
|
|
* [FastTrack][26]
|
|
* Partner
|
|
* [Partner Network][27]
|
|
* [Solution Providers][28]
|
|
* [Partner Center][29]
|
|
* [Cloud Hosting][30]
|
|
* Industries
|
|
* [Education][31]
|
|
* [Financial services][32]
|
|
* [Government][33]
|
|
* [Health][34]
|
|
* [Manufacturing & resources][35]
|
|
* [Retail][36]
|
|
* Other
|
|
* [Security][37]
|
|
* [Licensing][38]
|
|
* [AppSource][39]
|
|
* [Azure Marketplace][40]
|
|
* [Events][41]
|
|
* [View all][42]
|
|
|
|
[ Research ][43] [Research Home][43]
|
|
|
|
Research areas
|
|
|
|
* Intelligence
|
|
* [Artificial Intelligence][44]
|
|
* [Computer vision][45]
|
|
* [Graphics & multimedia][46]
|
|
* [Human-computer interaction][47]
|
|
* [Human language technologies][48]
|
|
* [Search & information retrieval][49]
|
|
* Systems
|
|
* [Data visualization, analytics & platform][50]
|
|
* [Hardware, devices & quantum computing][51]
|
|
* [Programming languages & software engineering][52]
|
|
* [Security, privacy & cryptography][53]
|
|
* [Systems & networking][54]
|
|
* Theory
|
|
* [Algorithms][55]
|
|
* [Mathematics][56]
|
|
* Other Sciences
|
|
* [Ecology & environment][57]
|
|
* [Economics][58]
|
|
* [Medical, health & genomics][59]
|
|
* [Social sciences][60]
|
|
* [Technology for emerging markets][61]
|
|
|
|
[Products & Downloads][62]
|
|
|
|
Programs & Events
|
|
|
|
* [Academic Programs][63]
|
|
* [Events & Conferences][64]
|
|
|
|
[People][65] [Careers][66]
|
|
|
|
Blogs & Podcasts
|
|
|
|
* [Microsoft Research Blog][67]
|
|
* [The Microsoft Research Podcast][68]
|
|
* [The AI Blog][69]
|
|
|
|
Labs & Locations
|
|
|
|
* Microsoft Research
|
|
* [MSR AI][70]
|
|
* [Asia Lab (Chinese)][71]
|
|
* [Asia Lab (English)][72]
|
|
* [Cambridge Lab][73]
|
|
* [India Lab][74]
|
|
* [Montreal Lab][75]
|
|
* [New England Lab][76]
|
|
* [New York City Lab][77]
|
|
* [Redmond Lab][78]
|
|
* Other labs/locations
|
|
* [Applied Sciences Lab][79]
|
|
* [Advanced Technology Lab Cairo][80]
|
|
* [Quantum][81]
|
|
* About
|
|
* [Research at Microsoft][82]
|
|
|
|
# Should Your Specification Language Be Typed?
|
|
|
|
May 4, 1999
|
|
|
|
* [ Download PDF ][83]
|
|
* [ BibTex ][84]
|
|
|
|
## Authors
|
|
|
|
* [Leslie Lamport][85]
|
|
* Lawrence C. Paulson
|
|
|
|
## Published In
|
|
|
|
ACM Transactions on Programming Languages and Systems. Also appeared as SRC Research Report 147.
|
|
|
|
## Publication Type
|
|
|
|
Article
|
|
|
|
## Pages
|
|
|
|
502-526
|
|
|
|
## Volume
|
|
|
|
21/3
|
|
|
|
* [ Abstract ][86]
|
|
* [ Related Info ][87]
|
|
|
|
## Abstract
|
|
|
|
In 1995, I wrote a diatribe titled Types Considered Harmful. It argued that, although types are good for programming languages, they are a bad way to formalize mathematics. This implies that they are bad for specification and verification, which should be mathematics rather than programming. My note apparently provoked some discussion, mostly disagreeing with it. I thought it might be fun to promote a wider discussion by publishing it, and TOPLAS was, for me, the obvious place. Andrew Appel, the editor-in-chief at the time, was favorably disposed to the idea, so I submitted it. Some of my arguments were not terribly sound, since I know almost nothing about type theory. The referees were suitably harsh, but Appel felt it would still be a good idea to publish a revised version along with rebuttals. I suggested that it would be better if I and the referees cooperated on a single balanced article presenting both sides of the issue. The two referees agreed to shed their anonymity and participate. Larry Paulson was one of the referees. It soon became apparent that Paulson and I could not work with the other referee, who was rabidly pro-types. (At one point, he likened his situation to someone being asked by a neo-Nazi to put his name on a “balanced” paper on racism.) So, Paulson and I wrote the paper by ourselves. We expected that the other referee would write a rebuttal, but he apparently never did.
|
|
|
|
## Related Info
|
|
|
|
## Research Areas
|
|
|
|
* [ Algorithms ][55]
|
|
|
|
## Follow Microsoft Research
|
|
|
|
* * [Follow @MSFTResearch][88]
|
|
* ## Share this page
|
|
* * [Tweet][89]
|
|
* #### What's new
|
|
* [Surface Book 2][90]
|
|
* [Surface Pro][91]
|
|
* [Xbox One X][92]
|
|
* [Xbox One S][93]
|
|
* [VR & mixed reality][94]
|
|
* [Windows 10 apps][95]
|
|
* [Office apps][96]
|
|
|
|
#### Store & Support
|
|
|
|
* [Account profile][97]
|
|
* [Download Center][98]
|
|
* [Sales & support][99]
|
|
* [Returns][100]
|
|
* [Order tracking][101]
|
|
* [Store locations][102]
|
|
* [Support][103]
|
|
* [Buy online, pick up in store][104]
|
|
|
|
#### Education
|
|
|
|
* [Microsoft in education][31]
|
|
* [Office for students][105]
|
|
* [Office 365 for schools][106]
|
|
* [Deals for students & educators ][107]
|
|
* [Microsoft Azure in education][108]
|
|
|
|
#### Enterprise
|
|
|
|
* [Microsoft Azure ][109]
|
|
* [Enterprise][110]
|
|
* [Data platform][111]
|
|
* [Find a solutions provider][112]
|
|
* [Microsoft partner resources ][113]
|
|
* [Microsoft AppSource ][114]
|
|
* [Manufacturing & resources][35]
|
|
* [Financial services][32]
|
|
|
|
#### Developer
|
|
|
|
* [Microsoft Visual Studio][14]
|
|
* [Windows Dev Center][24]
|
|
* [Developer Network][23]
|
|
* [TechNet][115]
|
|
* [Microsoft Virtual Academy][116]
|
|
* [Microsoft developer program][117]
|
|
* [Channel 9][118]
|
|
* [Office Dev Center][119]
|
|
|
|
#### Company
|
|
|
|
* [Careers][120]
|
|
* [About Microsoft][121]
|
|
* [Company news][122]
|
|
* [Privacy at Microsoft][123]
|
|
* [Investors][124]
|
|
* [Diversity and inclusion][125]
|
|
* [Accessibility][126]
|
|
* [Security][127]
|
|
* [Sitemap][128]
|
|
* [Contact us][129]
|
|
* [Privacy & cookies ][130]
|
|
* [Terms of use][131]
|
|
* [Trademarks][132]
|
|
* [About our ads][133]
|
|
* © Microsoft 2018
|
|
|
|
![][134]
|
|
|
|
[1]: https://go.microsoft.com/fwlink/?linkid=845480
|
|
[2]: https://img-prod-cms-rt-microsoft-com.akamaized.net/cms/api/am/imageFileData/RE1Mu3b?ver=5c31
|
|
[3]: https://www.microsoft.com
|
|
[4]: https://www.microsoft.com/en-us/microsoft-365
|
|
[5]: https://azure.microsoft.com
|
|
[6]: https://products.office.com/en-us/business/office
|
|
[7]: https://dynamics.microsoft.com/en-us/
|
|
[8]: https://www.microsoft.com/sql-server/
|
|
[9]: https://www.microsoft.com/en-us/windowsforbusiness
|
|
[10]: https://www.microsoft.com/cloud-platform/windows-server
|
|
[11]: https://www.microsoft.com/cloud-platform/enterprise-mobility-security
|
|
[12]: https://powerbi.microsoft.com/en-us/
|
|
[13]: https://products.office.com/en-us/microsoft-teams/group-chat-software
|
|
[14]: https://www.visualstudio.com/
|
|
[15]: https://www.microsoft.com/en-us/surface/business/overview
|
|
[16]: https://www.microsoft.com/ai/
|
|
[17]: https://www.microsoft.com/internet-of-things
|
|
[18]: https://azure.microsoft.com/services/cognitive-services/
|
|
[19]: https://www.microsoft.com/quantum/
|
|
[20]: https://www.microsoft.com/research/
|
|
[21]: https://docs.microsoft.com/en-us/
|
|
[22]: https://technet.microsoft.com/en-us/ms376608.aspx
|
|
[23]: https://msdn.microsoft.com/en-us
|
|
[24]: https://developer.microsoft.com/en-us/windows
|
|
[25]: https://www.microsoft.com/en-us/itpro/windows
|
|
[26]: https://fasttrack.microsoft.com/office
|
|
[27]: https://partner.microsoft.com/
|
|
[28]: https://www.microsoft.com/solution-providers/
|
|
[29]: https://partnercenter.microsoft.com/partner/home
|
|
[30]: https://www.microsoft.com/en-us/cloudandhosting
|
|
[31]: https://www.microsoft.com/en-us/education
|
|
[32]: https://enterprise.microsoft.com/en-us
|
|
[33]: https://enterprise.microsoft.com/en-us/industries/government/
|
|
[34]: https://enterprise.microsoft.com/en-us/industries/health/
|
|
[35]: https://enterprise.microsoft.com/en-us/industries/discrete-manufacturing/
|
|
[36]: https://enterprise.microsoft.com/en-us/industries/retail-and-consumer-goods/
|
|
[37]: https://www.microsoft.com/security/
|
|
[38]: https://www.microsoft.com/licensing/
|
|
[39]: https://appsource.microsoft.com/
|
|
[40]: https://azuremarketplace.microsoft.com/marketplace/
|
|
[41]: https://events.microsoft.com/
|
|
[42]: https://www.microsoft.com/en-us/sitemap.aspx
|
|
[43]: https://www.microsoft.com/en-us/research/
|
|
[44]: https://www.microsoft.com/en-us/research/research-area/artificial-intelligence/
|
|
[45]: https://www.microsoft.com/en-us/research/research-area/computer-vision/
|
|
[46]: https://www.microsoft.com/en-us/research/research-area/graphics-and-multimedia/
|
|
[47]: https://www.microsoft.com/en-us/research/research-area/human-computer-interaction/
|
|
[48]: https://www.microsoft.com/en-us/research/research-area/human-language-technologies/
|
|
[49]: https://www.microsoft.com/en-us/research/research-area/search-information-retrieval/
|
|
[50]: https://www.microsoft.com/en-us/research/research-area/data-visualization-analytics-platform/
|
|
[51]: https://www.microsoft.com/en-us/research/research-area/hardware-devices-quantum-computing/
|
|
[52]: https://www.microsoft.com/en-us/research/research-area/programming-languages-software-engineering/
|
|
[53]: https://www.microsoft.com/en-us/research/research-area/security-privacy-cryptography/
|
|
[54]: https://www.microsoft.com/en-us/research/research-area/systems-and-networking/
|
|
[55]: https://www.microsoft.com/en-us/research/research-area/algorithms/
|
|
[56]: https://www.microsoft.com/en-us/research/research-area/computational-sciences-mathematics/
|
|
[57]: https://www.microsoft.com/en-us/research/research-area/ecology-environment/
|
|
[58]: https://www.microsoft.com/en-us/research/research-area/economics/
|
|
[59]: https://www.microsoft.com/en-us/research/research-area/medical-health-genomics/
|
|
[60]: https://www.microsoft.com/en-us/research/research-area/social-sciences/
|
|
[61]: https://www.microsoft.com/en-us/research/research-area/technology-for-emerging-markets/
|
|
[62]: https://www.microsoft.com/en-us/research/products/
|
|
[63]: https://www.microsoft.com/en-us/research/academic-programs/
|
|
[64]: https://www.microsoft.com/en-us/research/events-conferences/
|
|
[65]: https://www.microsoft.com/en-us/research/people/
|
|
[66]: https://www.microsoft.com/en-us/research/careers/
|
|
[67]: https://www.microsoft.com/en-us/research/blog
|
|
[68]: https://www.microsoft.com/en-us/research/blog/category/podcast/
|
|
[69]: https://blogs.microsoft.com/next/
|
|
[70]: https://www.microsoft.com/en-us/research/lab/microsoft-research-ai/
|
|
[71]: http://www.msra.cn
|
|
[72]: https://www.microsoft.com/en-us/research/lab/microsoft-research-asia/
|
|
[73]: https://www.microsoft.com/en-us/research/lab/microsoft-research-cambridge/
|
|
[74]: https://www.microsoft.com/en-us/research/lab/microsoft-research-india/
|
|
[75]: https://www.microsoft.com/en-us/research/lab/microsoft-research-montreal/
|
|
[76]: https://www.microsoft.com/en-us/research/lab/microsoft-research-new-england/
|
|
[77]: https://www.microsoft.com/en-us/research/lab/microsoft-research-new-york/
|
|
[78]: https://www.microsoft.com/en-us/research/lab/microsoft-research-redmond/
|
|
[79]: https://www.microsoft.com/en-us/research/lab/applied-sciences-group/
|
|
[80]: https://www.microsoft.com/en-us/research/group/advanced-technology-lab-cairo-2/
|
|
[81]: https://www.microsoft.com/en-us/research/lab/quantum/
|
|
[82]: https://www.microsoft.com/en-us/research/about/
|
|
[83]: https://www.microsoft.com/en-us/research/uploads/prod/2016/12/Should-Your-Specification-Language-Be-Typed.pdf
|
|
[84]: https://www.microsoft.com/en-us/research/publication/specification-language-typed/bibtex/
|
|
[85]: https://www.microsoft.com/en-us/research/people/lamport/
|
|
[86]: https://www.microsoft.com#%21abstract
|
|
[87]: https://www.microsoft.com#%21related_info
|
|
[88]: https://twitter.com/MSFTResearch
|
|
[89]: https://twitter.com/share
|
|
[90]: https://www.microsoft.com/en-us/surface/devices/surface-book-2/overview
|
|
[91]: https://www.microsoft.com/en-us/surface/devices/surface-pro/overview
|
|
[92]: https://www.xbox.com/en-us/xbox-one-x
|
|
[93]: https://www.xbox.com/en-us/xbox-one-s?xr=shellnav
|
|
[94]: https://www.microsoft.com/en-us/store/b/virtualreality
|
|
[95]: https://www.microsoft.com/en-us/windows/windows-10-apps
|
|
[96]: https://store.office.com/en-us/appshome.aspx?
|
|
[97]: https://account.microsoft.com/
|
|
[98]: https://www.microsoft.com/en-us/download
|
|
[99]: https://go.microsoft.com/fwlink/p/?LinkID=824761&clcid=0x409
|
|
[100]: https://go.microsoft.com/fwlink/p/?LinkID=824764&clcid=0x409
|
|
[101]: https://account.microsoft.com/orders
|
|
[102]: https://www.microsoft.com/en-us/store/locations/find-a-store
|
|
[103]: https://support.microsoft.com/en-us
|
|
[104]: https://www.microsoft.com/en-us/store/b/buy-online-pick-up-in-store?icid=uhf_footer_bopuis
|
|
[105]: https://www.microsoft.com/en-us/education/products/office/default.aspx
|
|
[106]: https://products.office.com/en-us/academic/compare-office-365-education-plans
|
|
[107]: https://www.microsoft.com/en-us/store/b/student
|
|
[108]: https://azure.microsoft.com/en-us/community/education/
|
|
[109]: https://azure.microsoft.com/
|
|
[110]: https://enterprise.microsoft.com/en-us/
|
|
[111]: https://www.microsoft.com/en-us/sql-server/
|
|
[112]: https://www.microsoft.com/en-us/solution-providers
|
|
[113]: https://partner.microsoft.com/en-us/
|
|
[114]: https://go.microsoft.com/fwlink/?LinkID=808093
|
|
[115]: https://technet.microsoft.com/en-us
|
|
[116]: https://mva.microsoft.com/
|
|
[117]: https://developer.microsoft.com/en-us/store/register
|
|
[118]: https://channel9.msdn.com/
|
|
[119]: https://developer.microsoft.com/office
|
|
[120]: https://careers.microsoft.com/
|
|
[121]: https://www.microsoft.com/en-us/about
|
|
[122]: https://news.microsoft.com/
|
|
[123]: https://privacy.microsoft.com/en-us
|
|
[124]: https://www.microsoft.com/investor/default.aspx
|
|
[125]: https://www.microsoft.com/en-us/diversity/
|
|
[126]: https://www.microsoft.com/en-us/accessibility/home
|
|
[127]: https://www.microsoft.com/en-us/security/default.aspx
|
|
[128]: https://www.microsoft.com/en-us/sitemap1.aspx
|
|
[129]: https://support.microsoft.com/en-us/contactus
|
|
[130]: https://go.microsoft.com/fwlink/?LinkId=521839
|
|
[131]: https://go.microsoft.com/fwlink/?LinkID=206977
|
|
[132]: https://www.microsoft.com/trademarks
|
|
[133]: https://choice.microsoft.com
|
|
[134]: https://www.facebook.com/tr?id=435868603227390&ev=PageView&noscript=1
|
|
|