F* (programming language)

<h2 id="history">History</h2>
<h3>Versions</h3>
<p>Until version 2022.03.24, F* was written entirely in a common subset of F* and <a href="/facts/F_Sharp_(programming_language)/jdXHnYz5">F#</a> and supported bootstrapping in both <a href="/facts/OCaml/ThBGLND8">OCaml</a> and F#. This was dropped starting in version 2022.04.02.<a class="footnote-ref" id="fnref:5" href="#fn:5"><sup>5</sup></a><a class="footnote-ref" id="fnref:6" href="#fn:6"><sup>6</sup></a>
</p>
<h2 id="overview">Overview</h2>
<h3>Operators</h3>
<p>F* supports common arithmetic <a href="/facts/Operator_(computer_programming)/7TnU5LKu">operators</a> such as +, -, *, and /. Also, F* supports relational operators like <, <=, ==, !=, >, and >=.<a class="footnote-ref" id="fnref:7" href="#fn:7"><sup>7</sup></a>
</p>
<h3>Data types</h3>
<p>Common primitive <a href="/facts/Primitive_data_type/0c898228">data types</a> in F* are bool, int, float, char, and unit.<a class="footnote-ref" id="fnref:8" href="#fn:8"><sup>8</sup></a>
</p>

<h3>Sources</h3>
<ul><li>Ahman, Danel; Hriţcu, Cătălin; Maillard, Kenji; Martínez, Guido; Plotkin, Gordon; Protzenko, Jonathan; Rastogi, Aseem; Swamy, Nikhil (2017). <a href="https://fstar-lang.org/papers/dm4free/">"Dijkstra Monads for Free"</a>. <i>44nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages</i>.</li>
<li>Swamy, Nikhil; Hriţcu, Cătălin; Keller, Chantal; Rastogi, Aseem; Delignat-Lavaud, Antoine; Forest, Simon; Bhargavan, Karthikeyan; Fournet, Cédric; Strub, Pierre-Yves; Kohlweiss, Markulf; Zinzindohoue, Jean-Karim; Zanella-Béguelin, Santiago (2016). <a href="https://fstar-lang.org/papers/mumon/">"Dependent Types and Multi-Monadic Effects in F*"</a>. <i>43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages</i>.</li>
<li>Swamy, Nikhil; Martínez, Guido; Rastogi, Aseem (2024). <i><a href="https://fstar-lang.org/tutorial/proof-oriented-programming-in-fstar.pdf">Proof-Orented Programming in F*</a>.</i></li></ul>
<h2 id="external-links">External links</h2>
<ul><li><a href="http://fstar-lang.org">Official website</a></li>
<li><a href="https://github.com/FStarLang">FStarLang</a> on <a href="/facts/GitHub/n1hNCsc3">GitHub</a></li>
<li><a href="https://fstar-lang.org/tutorial/">F* tutorial</a></li></ul>

<h2 id="references">References</h2>

<ol>
<li id="fn:1"><p>"Microsoft Research Inria Joint Centre". MSR-INRIA. <a href="https://www.microsoft.com/en-us/research/collaboration/inria-joint-centre/" target="_blank">https://www.microsoft.com/en-us/research/collaboration/inria-joint-centre/</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></p></li>
<li id="fn:2"><p>Swamy, Nikhil; Chen, Juan; Fournet, Cédric; Strub, Pierre-Yves; Bhargavan, Karthikeyan; Yang, Jean (September 2011). Secure distributed programming with value-dependent types. ICFP '11: Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming. Vol. 46. Tokyo, Japan: Association for Computing Machinery. pp. 266–278. doi:10.1145/2034574.2034811. Retrieved 17 April 2023. <a href="https://dl.acm.org/doi/10.1145/2034773.2034811" target="_blank">https://dl.acm.org/doi/10.1145/2034773.2034811</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></p></li>
<li id="fn:3"><p>"The F* Project". Microsoft. Retrieved 20 April 2023. <a href="https://www.microsoft.com/en-us/research/project/the-f-project/" target="_blank">https://www.microsoft.com/en-us/research/project/the-f-project/</a> <a href="#fnref:3" class="footnote-back-ref">↩</a></p></li>
<li id="fn:4"><p>"FStarLang/FStar". GitHub. Retrieved 23 April 2024. <a href="https://github.com/FStarLang/FStar" target="_blank">https://github.com/FStarLang/FStar</a> <a href="#fnref:4" class="footnote-back-ref">↩</a></p></li>
<li id="fn:5"><p>"fstar.exe is no longer buildable in F# as a .NET executable #2512". Github. Retrieved 17 April 2023. <a href="https://github.com/FStarLang/FStar/pull/2512" target="_blank">https://github.com/FStarLang/FStar/pull/2512</a> <a href="#fnref:5" class="footnote-back-ref">↩</a></p></li>
<li id="fn:6"><p>"Consider dropping requirement that F* code has to be valid F# #1737". Github. Retrieved 17 April 2023. <a href="https://github.com/FStarLang/FStar/issues/1737" target="_blank">https://github.com/FStarLang/FStar/issues/1737</a> <a href="#fnref:6" class="footnote-back-ref">↩</a></p></li>
<li id="fn:7"><p>Swamy, Nikhil; Martínez, Guido; Rastogi, Aseem (Jan 14, 2024). Proof-Oriented Programming in F* (PDF). <a href="https://fstar-lang.org/tutorial/proof-oriented-programming-in-fstar.pdf" target="_blank">https://fstar-lang.org/tutorial/proof-oriented-programming-in-fstar.pdf</a> <a href="#fnref:7" class="footnote-back-ref">↩</a></p></li>
<li id="fn:8"><p>Swamy, Nikhil; Martínez, Guido; Rastogi, Aseem (Jan 14, 2024). Proof-Oriented Programming in F* (PDF). <a href="https://fstar-lang.org/tutorial/proof-oriented-programming-in-fstar.pdf" target="_blank">https://fstar-lang.org/tutorial/proof-oriented-programming-in-fstar.pdf</a> <a href="#fnref:8" class="footnote-back-ref">↩</a></p></li>
</ol>

F* (programming language) open-in-new

F* (programming language)