#15569: Constant folding optimises 1 into 3 -------------------------------------+------------------------------------- Reporter: snowleopard | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1-beta1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9136 | Differential Rev(s): Phab:D5109 Wiki Page: | -------------------------------------+------------------------------------- Comment (by flip101): Since the phrases "SMT solver" and "compiler-checked way" came up. Wouldn't it be good for GHC to move into the direction that CakeML has chosen and then (at least for some parts) verify the compiler with proof? It could be a good addition to CI and also for local builds to run after the test suite. Excuse me if the question is too broad of scope, but the ticket seems a good example for it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15569#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler